Hostname: page-component-cd9895bd7-lnqnp Total loading time: 0 Render date: 2024-12-24T16:26:28.586Z Has data issue: false hasContentIssue false
  • English
  • Français

Characteristic Formulae for Timed Automata

Published online by Cambridge University Press:  15 April 2002

Luca Aceto ,
Anna Ingólfsdóttir ,
Mikkel Lykke Pedersen  and
Jan Poulsen
Luca Aceto
Affiliation:
(asic esearch in omputer cience, Centre of the Danish National Research Foundation), Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark.
Anna Ingólfsdóttir
Affiliation:
(asic esearch in omputer cience, Centre of the Danish National Research Foundation), Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark.
Mikkel Lykke Pedersen
Affiliation:
(asic esearch in omputer cience, Centre of the Danish National Research Foundation), Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark.
Jan Poulsen
Affiliation:
(asic esearch in omputer cience, Centre of the Danish National Research Foundation), Department of Computer Science, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark.
Get access

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.

Keywords

Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 34 , Issue 6 , November 2000 , pp. 565 - 584
Copyright
© EDP Sciences, 2000

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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.
Alur, R. and Dill, D.L., A theory of timed automata. Theoret. Comput. Sci. 126 (1994) 183-235. (Fundamental Study). CrossRef
Arun-Kumar, S. and Hennessy, M., An efficiency preorder for processes. Acta Inform. 29 (1992) 737-760. CrossRef
J. Baeten and J. Klop, in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990).
Bloom, B., Istrail, S. and Meyer, A.R., Bisimulation can't be traced. J. Assoc. Comput. Mach. 42 (1995) 232-268. CrossRef
Browne, M., Clarke, E. and Grümberg, O., Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988) 115-131. CrossRef
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 Design 2 (1993) 121-147. CrossRef
Engelfriet, J., Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci. 36 (1985) 21-25. CrossRef
R.J.V. Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [], pp. 278-297.
Graf, S. and Sifakis, J., A modal characterization of observational congruence on finite terms of CCS. Inform. and Control 68 (1986) 125-145. CrossRef
Hennessy, M. and Milner, R., Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach. 32 (1985) 137-161. CrossRef
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).
Keller, R., Formal verification of parallel programs. Comm. ACM 19 (1976) 371-384. CrossRef
Kozen, D., Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. CrossRef
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 20 th 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.
Larsen, K.G. and Skou, A., Bisimulation through probabilistic testing. Inform. and Comput. 94 (1991) 1-28. CrossRef
R. Milner, An algebraic definition of simulation between programs, in Proc. 2 nd 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: 2 nd 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 5 th 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).
Steffen, B. and Ingólfsdóttir, A., Characteristic formulae for processes with divergence. Inform. and Comput. 110 (1994) 149-163. CrossRef
Tarski, A., A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5 (1955) 285-309. CrossRef
Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [], pp. 502-520.