# Characteristic Formulae for Timed Automata

Luca Aceto; Anna Ingólfsdóttir; Mikkel Lykke Pedersen; Jan Poulsen

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 34, Issue: 6, page 565-584
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topAceto, Luca, et al. "Characteristic Formulae for Timed Automata." RAIRO - Theoretical Informatics and Applications 34.6 (2010): 565-584. <http://eudml.org/doc/222071>.

@article{Aceto2010,

abstract = {
This paper offers characteristic formula constructions in the
real-time logic Lν for several behavioural relations between
(states of) timed automata. The behavioural relations studied in
this work are timed (bi)similarity, timed ready simulation,
faster-than bisimilarity and timed trace inclusion. The
characteristic formulae delivered by our constructions have size
which is linear in that of the timed automaton they logically
describe. This also applies to the characteristic formula for timed
bisimulation equivalence, for which an exponential space
construction was previously offered by Laroussinie, Larsen and
Weise.
},

author = {Aceto, Luca, Ingólfsdóttir, Anna, Pedersen, Mikkel Lykke, Poulsen, Jan},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {real-time logic; timed bisimulation equivalence},

language = {eng},

month = {3},

number = {6},

pages = {565-584},

publisher = {EDP Sciences},

title = {Characteristic Formulae for Timed Automata},

url = {http://eudml.org/doc/222071},

volume = {34},

year = {2010},

}

TY - JOUR

AU - Aceto, Luca

AU - Ingólfsdóttir, Anna

AU - Pedersen, Mikkel Lykke

AU - Poulsen, Jan

TI - Characteristic Formulae for Timed Automata

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 34

IS - 6

SP - 565

EP - 584

AB -
This paper offers characteristic formula constructions in the
real-time logic Lν for several behavioural relations between
(states of) timed automata. The behavioural relations studied in
this work are timed (bi)similarity, timed ready simulation,
faster-than bisimilarity and timed trace inclusion. The
characteristic formulae delivered by our constructions have size
which is linear in that of the timed automaton they logically
describe. This also applies to the characteristic formula for timed
bisimulation equivalence, for which an exponential space
construction was previously offered by Laroussinie, Larsen and
Weise.

LA - eng

KW - real-time logic; timed bisimulation equivalence

UR - http://eudml.org/doc/222071

ER -

## References

top- L. Aceto and F. Laroussinie, Is your model checker on time? On the complexity of model checking for timed modal logics. Springer-Verlag, Berlin, Math. Foundations of Comput. Sci. 1999 (Szklarska Poreba) (1999) 125-136.
- R. Alur and D.L. Dill, A theory of timed automata. Theoret. Comput. Sci.126 (1994) 183-235. (Fundamental Study).
- S. Arun-Kumar and M. Hennessy, An efficiency preorder for processes. Acta Inform.29 (1992) 737-760.
- J. Baeten and J. Klop, in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990).
- B. Bloom, S. Istrail and A.R. Meyer, Bisimulation can't be traced. J. Assoc. Comput. Mach.42 (1995) 232-268.
- M. Browne, E. Clarke and O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci.59 (1988) 115-131.
- E. Clarke and E. Emerson, Design and synthesis of synchronization skeletons using branching-time temporal logic, in Proc. of the Workshop on Logic of Programs, Yorktown Heights, edited by D. Kozen. Springer-Verlag, Lecture Notes in Comput. Sci. 131 (1981) 52-71.
- E. Clarke, O. Grümberg and D. Peled, Model Checking. MIT Press (2000).
- R. Cleaveland and B. Steffen, Computing behavioral relations, logically, in ICALP '91: Automata, Languages and Programming, edited by J.L. Albert, B. Monien and M.R. Artalejo. Springer-Verlag, Lecture Notes in Comput. Sci. 510 (1991) 127-138.
- height 2pt depth -1.6pt width 23pt, A linear-time model-checking algorithm for the alternation-free modal µ-calculus. Formal Methods in Systems Design2 (1993) 121-147.
- J. Engelfriet, Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci.36 (1985) 21-25.
- R.J.V. Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [], pp. 278-297.
- S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS. Inform. and Control68 (1986) 125-145.
- M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach.32 (1985) 137-161.
- A. Ingólfsdóttir, J.C. Godskesen and M. Zeeberg, Fra Hennessy-Milner logik til CCS-processer. Master's thesis, Department of Computer Science, Aalborg University (1987).
- R. Keller, Formal verification of parallel programs. Comm. ACM19 (1976) 371-384.
- D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci.27 (1983) 333-354.
- F. Laroussinie and K.G. Larsen, CMC: A tool for compositional model-checking of real-time systems, in Proc. IFIP Joint Int. Conf. Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PS TV'98). Kluwer Academic Publishers (1998) 439-456.
- F. Laroussinie, K.G. Larsen and C. Weise, From timed automata to logic - and back, in Proc. of the 20th Symposium on Mathematical Foundations of Computer Science. Springer-Verlag, Lecture Notes in Comput. Sci. 969 (1995) 529-540.
- F. Laroussinie and P. Schnoebelen, The state explosion problem from trace to bisimulation equivalence, in Proc. of the 3rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS'2000). Springer-Verlag, Lecture Notes in Comput. Sci. 1784 (2000) 192-207.
- K.G. Larsen and A. Skou, Bisimulation through probabilistic testing. Inform. and Comput.94 (1991) 1-28.
- R. Milner, An algebraic definition of simulation between programs, in Proc. 2nd Joint Conference on Artificial Intelligence. William Kaufmann (1971) 481-489. Also available as Report No. CS-205, Computer Science Department, Stanford University.
- height 2pt depth -1.6pt width 23pt, Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989).
- F. Moller and C. Tofts, Relating processes with respect to speed, in CONCUR '91: 2nd International Conference on Concurrency Theory, edited by J.C.M. Baeten and J.F. Groote. Springer-Verlag, Amsterdam, The Netherlands, Lecture Notes in Comput. Sci. 527 (1991) 424-438.
- D. Park, Concurrency and automata on infinite sequences, in 5th GI Conference, Karlsruhe, Germany, edited by P. Deussen. Springer-Verlag, Lecture Notes in Comput. Sci. 104 (1981) 167-183.
- M.L. Pedersen and J. Poulsen, Model-checking characteristic formulae -- a method for proving timed behavioural relations. Master's thesis, Department of Computer Science, Aalborg University (1999).
- B. Steffen and A. Ingólfsdóttir, Characteristic formulae for processes with divergence. Inform. and Comput.110 (1994) 149-163.
- A. Tarski, A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math.5 (1955) 285-309.
- Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [], pp. 502-520.

## Citations in EuDML Documents

top## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.