From timed automata to logic -- and back

DOI10.1007/3-540-60246-1_158MaRDI QIDQ3569043zbMATHOpenAlexFDO

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)

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

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)