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

Abstract

top
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.

How to cite

top

Aceto, 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
  1. 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.  
  2. R. Alur and D.L. Dill, A theory of timed automata. Theoret. Comput. Sci.126 (1994) 183-235. (Fundamental Study).  
  3. S. Arun-Kumar and M. Hennessy, An efficiency preorder for processes. Acta Inform.29 (1992) 737-760.  
  4. J. Baeten and J. Klop, in Proc. CONCUR 90, Amsterdam. Springer-Verlag, Lecture Notes in Comput. Sci. 458 (1990).  
  5. B. Bloom, S. Istrail and A.R. Meyer, Bisimulation can't be traced. J. Assoc. Comput. Mach.42 (1995) 232-268.  
  6. M. Browne, E. Clarke and O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci.59 (1988) 115-131.  
  7. 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.  
  8. E. Clarke, O. Grümberg and D. Peled, Model Checking. MIT Press (2000).  
  9. 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.  
  10. 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.  
  11. J. Engelfriet, Determinacy → (observation equivalence = trace equivalence). Theoret. Comput. Sci.36 (1985) 21-25.  
  12. R.J.V. Glabbeek, The linear time - branching time spectrum, in Baeten and Klop [], pp. 278-297.  
  13. S. Graf and J. Sifakis, A modal characterization of observational congruence on finite terms of CCS. Inform. and Control68 (1986) 125-145.  
  14. M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach.32 (1985) 137-161.  
  15. 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).  
  16. R. Keller, Formal verification of parallel programs. Comm. ACM19 (1976) 371-384.  
  17. D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci.27 (1983) 333-354.  
  18. 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.  
  19. 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.  
  20. 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.  
  21. K.G. Larsen and A. Skou, Bisimulation through probabilistic testing. Inform. and Comput.94 (1991) 1-28.  
  22. 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.  
  23. height 2pt depth -1.6pt width 23pt, Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989).  
  24. 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.  
  25. 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.  
  26. 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).  
  27. B. Steffen and A. Ingólfsdóttir, Characteristic formulae for processes with divergence. Inform. and Comput.110 (1994) 149-163.  
  28. A. Tarski, A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math.5 (1955) 285-309.  
  29. Y. Wang, Real-time behaviour of asynchronous agents, in Baeten and Klop [], pp. 502-520.  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.