From timed automata to logic -- and back

DOI10.1007/3-540-60246-1_158MaRDI QIDQ3569043zbMATH OpenOpenAlexFDO

Authors François Laroussinie, Carsten Weise, Kim G. Larsen

Publication date 17 June 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-60246-1_158

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Recommendations

• Characteristic formulae for timed autoamta
• A Logical Characterisation of Event Clock Automata
• A theory of timed automata
• scientific article; zbMATH DE number 1256652
• Verification of timed automata via satisfiability checking

Cited in

(24)

• A Logical Characterisation of Event Clock Automata
• Alternation-free weighted mu-calculus: decidability and completeness
• Timed modal logics for real-time systems. Specification, verification and control
• scientific article; zbMATH DE number 1927567 (Why is no real title available?)
• Adequacy and complete axiomatization for timed modal logic
• Timed tree automata with an application to temporal logic.
• Characteristic formulae for fixed-point semantics: a general framework
• Timed Control with Observation Based and Stuttering Invariant Strategies
• Learning deterministic probabilistic automata from a model checking perspective
• Pushdown timed automata: A binary reachability characterization and safety verification.
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Presburger liveness verification of discrete timed automata.
• Non-interference control synthesis for security timed automata
• Monotonic hybrid systems
• Generalized discrete timed automata: Decidable approximations for safety verification.
• The power of reachability testing for timed automata
• Characteristic formulae for timed autoamta
• Composition methods for constructing characteristic formulas for dense-time models
• On decidability of recursive weighted logics
• On characteristic formulae for event-recording automata
• A menagerie of timed automata
• Model-checking for real-time systems
• Logics meet 1-clock alternating timed automata
• Simulation relations and applications in formal methods

This page was built for publication: From timed automata to logic -- and back

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3569043)