Hostname: page-component-cd9895bd7-gvvz8 Total loading time: 0 Render date: 2024-12-24T13:34:54.004Z Has data issue: false hasContentIssue false
  • English
  • Français

On characteristic formulae for Event-Recording Automata∗

Published online by Cambridge University Press:  10 January 2013

Omer Landry Nguena Timo  and
Pierre-Alain Reynier
Omer Landry Nguena Timo
Affiliation:
Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université Bordeaux 1, 351 cours de la Libération, 33405 Talence Cedex, France.. [email protected]
Pierre-Alain Reynier
Affiliation:
Laboratoire d’Informatique Fondamentale (LIF), Aix-Marseille Université, 39 avenue Joliot-Curie, 13453 Marseille Cedex 13, France.; [email protected]
Get access

Abstract

A standard bridge between automata theory and logic is provided by the notion ofcharacteristic formula. This paper investigates this problem for the class ofevent-recording automata (ERA), a subclass of timed automata in which clocks areassociated with actions and that enjoys very good closure properties. We first study theproblem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), alogic introduced by Sorea to express event-based timed specifications. We prove that theconstruction proposed by Sorea for ERA without invariants is incorrect. More generally, weprove 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 logicWTμ , a new logic for event-based timed specificationscloser to the timed logic ℒν that was introduced byLaroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , andthat its model-checking problem against ERA is EXPTIME -complete. Finally, we providecharacteristic formulae constructions in WTμ forcharacterizing the general class of ERA up to timed (bi)similarity and study thecomplexity issues.

Keywords

Timed Logicbisimulationevent-clock automata
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 47 , Issue 1 , January 2013 , pp. 69 - 96
Copyright
© EDP Sciences 2013

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

Aceto, L., Ingólfsdóttir, A., Pedersen, M.L. and Poulsen, J., Characteristic formulae for timed automata. Theor. Inf. Appl. 34 (2000) 565–584. Google Scholar
Aceto, L. and Laroussinie, F., 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. Google Scholar
Alur, R. and Dill, D., A theory of timed automata, Theor. Comput. Sci. 126 (1994) 183–235. Google Scholar
Alur, R., Fix, L. and Henzinger, T.A., Event-clock automata : A determinizable class of timed automata. Theor. Comput. Sci. 211 (1999) 253–273. Google Scholar
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.
Bouyer, P., Cassez, F. and Laroussinie, F., Timed modal logics for real-time systems : Specification, verification and control. J. Logic Lang. Inform. 20 (2011) 169–203. Google Scholar
Chandra, A.K., D. Kozen and L.J. Stockmeyer, Alternation. J. ACM 28 (1981) 114–133. Google Scholar
Cleaveland, R. and Steffen, B., A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Method Syst. Design 2 (1993) 121–147. Google Scholar
D'Souza, D., A logical characterisation of event clock automata. Int. J. Found. Comput. Sci. 14 (2003) 625–640. Google Scholar
Henzinger, T.A., Nicollin, X., Sifakis, J. and Yovine, S., Symbolic model-checking for real-time systems. Inf. Comput. 111 (1994) 193–244. Google Scholar
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.
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.
O.L. Nguena Timo, Synthesis for a Weak Real-Time Logic, Ph.D. thesis, Université Bordeaux 1 (2009).
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.
Raskin, J.-F. and Schobbens, P.-Y., The logic of event clocks – decidability, complexity and expressiveness. J. Autom. Lang. Comb. 4 (1999) 247–286. Google Scholar
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.
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.
M. Sorea, Verification of Real-Time Systems through Lazy Approximations, Ph.D. thesis, Universität Ulm (2004).
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.