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

DOI10.1007/s10849-010-9127-4zbMath1216.68158OpenAlexW1550995752MaRDI QIDQ548704

François Laroussinie, Patricia Bouyer, Franck Cassez

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

timed automatamodel checkingtimed 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)

Related Items (3)

The mu-calculus and Model Checking ⋮ Unnamed Item ⋮ A menagerie of timed automata

Uses Software

• Kronos
• Uppaal
• CMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• A complete axiomatisation for observational congruence of finite-state behaviours
• A theory of timed automata
• Symbolic model checking for real-time systems
• The power of reachability testing for timed automata
• Games for synthesis of controllers with partial observation.
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Is your model checker on time? On the complexity of model checking for timed modal logics
• On the expressiveness of TPTL and MTL
• Characteristic Formulae for Timed Automata
• From timed automata to logic — and back
• Automata for the modal μ-calculus and related results
• A really temporal logic
• The benefits of relaxing punctuality
• On the synthesis of discrete controllers for timed systems
• On the decidability and complexity of Metric Temporal Logic over finite words
• CONCUR 2005 – Concurrency Theory

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