Timed modal logics for real-time systems. Specification, verification and control

DOI10.1007/S10849-010-9127-4MaRDI QIDQ548704zbMATH OpenOpenAlexFDO

Authors Patricia Bouyer, Franck Cassez, François Laroussinie

Publication date 30 June 2011

Published in Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10849-010-9127-4

zbMATH Keywords

model checkingtimed automatatimed modal logictimed control

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• CONCUR 2005 – Concurrency Theory
• Model-checking timed temporal logics
• Real-time logics: Complexity and expressiveness
• scientific article; zbMATH DE number 1304997
• Model-checking in dense real-time

Cites work

• scientific article; zbMATH DE number 1670789 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2085321 (Why is no real title available?)
• A complete axiomatisation for observational congruence of finite-state behaviours
• A really temporal logic
• A theory of timed automata
• Automata for the modal \(\mu \)-calculus and related results
• CONCUR 2005 – Concurrency Theory
• Characteristic formulae for timed autoamta
• From timed automata to logic -- and back
• Games for synthesis of controllers with partial observation.
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Kronos: A verification tool for real-time systems
• Model-checking in dense real-time
• On the decidability and complexity of Metric Temporal Logic over finite words
• On the expressiveness of TPTL and MTL
• On the synthesis of discrete controllers for timed systems
• Symbolic model checking for real-time systems
• The benefits of relaxing punctuality
• The power of reachability testing for timed automata
• Uppaal in a nutshell

Cited in

(20)

• Real-time logics: Complexity and expressiveness
• Model-checking timed temporal logics
• A survey on temporal logics for specifying and verifying real-time systems
• Verifying complex continuous real-time systems with coinductive CLP(R)
• Modularity for timed and hybrid systems
• scientific article; zbMATH DE number 1670577 (Why is no real title available?)
• scientific article; zbMATH DE number 1390056 (Why is no real title available?)
• CONCUR 2005 – Concurrency Theory
• Integrated Formal Methods
• scientific article; zbMATH DE number 176150 (Why is no real title available?)
• The mu-calculus and Model Checking
• Guest editorial: Special issue on formal modeling and analysis of timed systems
• CONCUR 2005 – Concurrency Theory
• Refinement and Consistency of Timed Modal Specifications
• Verification of \(N\)-\(M\) switching control system: a case study in temporal logic model checking
• Real-time semantics of state transition for embedded control systems
• scientific article; zbMATH DE number 1949604 (Why is no real title available?)
• Is your model checker on time? On the complexity of model checking for timed modal logics
• scientific article; zbMATH DE number 7455750 (Why is no real title available?)
• A menagerie of timed automata

Describes a project that uses

Uses Software

• Kronos
• Uppaal
• CMC

This page was built for publication: Timed modal logics for real-time systems. Specification, verification and control

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