On characteristic formulae for Event-Recording Automata

Omer Landry Nguena Timo; Pierre-Alain Reynier

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2013)

  • Volume: 47, Issue: 1, page 69-96
  • ISSN: 0988-3754

Abstract

top
A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that the construction proposed by Sorea for ERA without invariants is incorrect. More generally, we prove that timed bisimilarity cannot in general be expressed in ERL for the class of ERA , and study under which conditions on ERA it can be. Then, we introduce the logic WTμ , a new logic for event-based timed specifications closer to the timed logic ℒν that was introduced by Laroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , and that its model-checking problem against ERA is EXPTIME -complete. Finally, we provide characteristic formulae constructions in WTμ for characterizing the general class of ERA up to timed (bi)similarity and study the complexity issues.

How to cite

top

Nguena Timo, Omer Landry, and Reynier, Pierre-Alain. "On characteristic formulae for Event-Recording Automata." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 47.1 (2013): 69-96. <http://eudml.org/doc/273070>.

@article{NguenaTimo2013,
abstract = {A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that the construction proposed by Sorea for ERA without invariants is incorrect. More generally, we prove that timed bisimilarity cannot in general be expressed in ERL for the class of ERA , and study under which conditions on ERA it can be. Then, we introduce the logic WTμ , a new logic for event-based timed specifications closer to the timed logic ℒν that was introduced by Laroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , and that its model-checking problem against ERA is EXPTIME -complete. Finally, we provide characteristic formulae constructions in WTμ for characterizing the general class of ERA up to timed (bi)similarity and study the complexity issues.},
author = {Nguena Timo, Omer Landry, Reynier, Pierre-Alain},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {timed logic; bisimulation; event-clock automata; timed automata; timed bisimulation; timed mu-calculus; model checking},
language = {eng},
number = {1},
pages = {69-96},
publisher = {EDP-Sciences},
title = {On characteristic formulae for Event-Recording Automata},
url = {http://eudml.org/doc/273070},
volume = {47},
year = {2013},
}

TY - JOUR
AU - Nguena Timo, Omer Landry
AU - Reynier, Pierre-Alain
TI - On characteristic formulae for Event-Recording Automata
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2013
PB - EDP-Sciences
VL - 47
IS - 1
SP - 69
EP - 96
AB - A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that the construction proposed by Sorea for ERA without invariants is incorrect. More generally, we prove that timed bisimilarity cannot in general be expressed in ERL for the class of ERA , and study under which conditions on ERA it can be. Then, we introduce the logic WTμ , a new logic for event-based timed specifications closer to the timed logic ℒν that was introduced by Laroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , and that its model-checking problem against ERA is EXPTIME -complete. Finally, we provide characteristic formulae constructions in WTμ for characterizing the general class of ERA up to timed (bi)similarity and study the complexity issues.
LA - eng
KW - timed logic; bisimulation; event-clock automata; timed automata; timed bisimulation; timed mu-calculus; model checking
UR - http://eudml.org/doc/273070
ER -

References

top
  1. [1] L. Aceto, A. Ingólfsdóttir, M.L. Pedersen and J. Poulsen, Characteristic formulae for timed automata. Theor. Inf. Appl.34 (2000) 565–584. Zbl0974.68121MR1844719
  2. [2] L. Aceto and F. Laroussinie, Is your model-checker on time? On the complexity of model checking for timed modal logics. J. Log. Algebr. Program. 52–53 (2002) 7–51. Zbl1008.68030MR1943502
  3. [3] R. Alur and D. Dill, A theory of timed automata, Theor. Comput. Sci.126 (1994) 183–235. Zbl0803.68071MR1271580
  4. [4] R. Alur, L. Fix and T.A. Henzinger, Event-clock automata: A determinizable class of timed automata. Theor. Comput. Sci.211 (1999) 253–273. Zbl0912.68132MR1663893
  5. [5] H. Bekić, Definable operation in general algebras, and the theory of automata and flowcharts, in Programming Languages and Their Definition, edited by C.B. Jones. Springer. Lect. Notes Comput. Sci. 177 (1984) 30–55. Zbl0548.68004
  6. [6] P. Bouyer, F. Cassez and F. Laroussinie, Timed modal logics for real-time systems: Specification, verification and control. J. Logic Lang. Inform.20 (2011) 169–203. Zbl1216.68158MR2782114
  7. [7] A.K. Chandra, D. Kozen and L.J. Stockmeyer, Alternation. J. ACM28 (1981) 114–133. Zbl0473.68043MR603186
  8. [8] R. Cleaveland and B. Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Method Syst. Design2 (1993) 121–147. Zbl0772.68038MR1236233
  9. [9] D. D'Souza, A logical characterisation of event clock automata. Int. J. Found. Comput. Sci.14 (2003) 625–640. Zbl1101.68647MR2010588
  10. [10] T.A. Henzinger, X. Nicollin, J. Sifakis and S. Yovine, Symbolic model-checking for real-time systems. Inf. Comput.111 (1994) 193–244. Zbl0806.68080MR1276749
  11. [11] F. Laroussinie and K.G. Larsen, CMC : A tool for compositional model-checking of real-time systems, in Proc. of IFIP TC6 WG6.1 Joint Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE XI, and Protocol Specification, Testing and Verification, PSTV XVIII (Paris, Nov. 1998), edited by S. Budkowski, A.R. Cavalli and E. Najm, Kluwer, IFIP Conference Proceedings 135 (1998) 439–456. 
  12. [12] F. Laroussinie, K.G. Larsen and C. Weise, From timed automata to logic – and back, in Proc. of 20th Int. Symp. on Mathematical Foundations of Computer Science, MFCS ’95 (Prague, Aug./Sept. 1995), edited by J. Wiedermann and P. Hájek, Springer. Lect. Notes Comput. Sci. 969 (1995) 529–539. Zbl1193.03069MR1467280
  13. [13] O.L. Nguena Timo, Synthesis for a Weak Real-Time Logic, Ph.D. thesis, Université Bordeaux 1 (2009). 
  14. [14] O.L. Nguena Timo and P.-A. Reynier, On characteristic formulae for event-recording automata, in Proc. of 6th Workshop on Fixed Points in Computer Science, FICS ’09 (Coimbra, Sept. 2009), edited by R. Matthes and T. Uustalu. Inst. of Cybernetics, Tallinn (2009) 70–78. Zbl06198059
  15. [15] J.-F. Raskin and P.-Y. Schobbens, The logic of event clocks – decidability, complexity and expressiveness. J. Autom. Lang. Comb.4 (1999) 247–286. Zbl0978.03015MR1719363
  16. [16] D. Sangiorgi, Bisimulation : From the origins to today, in Proc. of 19th Ann. IEEE Symp. on Logic in Computer Science, LICS ’04 (Turku, July 2004). IEEE CS Press (2004) 298–302. 
  17. [17] M. Sorea, A decidable fixpoint logic for time-outs, in Proc. of 13th Int. Conf. on Concurrency Theory, CONCUR 2002 (Brno, Aug. 2002), edited by L. Brim, P. Jancar, M. Křetínský and A. Kučera, Springer. Lect. Notes Comput. Sci. 2421 (2002) 255–271. Zbl1012.03042MR2053810
  18. [18] M. Sorea, Verification of Real-Time Systems through Lazy Approximations, Ph.D. thesis, Universität Ulm (2004). 
  19. [19] W. Thomas, Languages, automata and logic, in Handbook of Formal Languages, Beyond Words, edited by G. Rozenberg and A. Salomaa. Springer 3 (1997) 389–455. Zbl0866.68057MR1470024

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.