Model-checking timed temporal logics

DOI10.1016/J.ENTCS.2009.02.044MaRDI QIDQ4982129zbMATH OpenOpenAlexFDO

Authors Patricia Bouyer

Publication date 23 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.02.044

zbMATH Keywords

model checkingtemporal logicstimed systems

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Model Checking Real-Time Systems
• scientific article; zbMATH DE number 1304997
• Model-checking in dense real-time
• A survey on temporal logics for specifying and verifying real-time systems
• Timed modal logics for real-time systems. Specification, verification and control

Cites work

• A really temporal logic
• A theory of timed automata
• Alternating finite automata on -words
• Alternating timed automata
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Axioms for real-time logics
• CONCUR 2005 – Concurrency Theory
• Costs Are Expensive!
• Counter-Free Input-Determined Timed Automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Foundations of Software Science and Computation Structures
• Foundations of Software Science and Computational Structures
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 1705164 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 1256652 (Why is no real title available?)
• scientific article; zbMATH DE number 1304997 (Why is no real title available?)
• scientific article; zbMATH DE number 1794360 (Why is no real title available?)
• scientific article; zbMATH DE number 1794367 (Why is no real title available?)
• scientific article; zbMATH DE number 2112984 (Why is no real title available?)
• scientific article; zbMATH DE number 5587267 (Why is no real title available?)
• HyTech: A model checker for hybrid systems
• Improved undecidability results on weighted timed automata
• Model-checking in dense real-time
• Model-Checking One-Clock Priced Timed Automata
• On Communicating Finite-State Machines
• On Expressiveness and Complexity in Real-Time Model Checking
• On the decidability and complexity of Metric Temporal Logic over finite words
• On the Expressiveness of MTL with Past Operators
• Real-time logics: Complexity and expressiveness
• Symbolic model checking for real-time systems
• The benefits of relaxing punctuality
• The benefits of relaxing punctuality
• Uppaal in a nutshell
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Weighted timed automata: model-checking and games
• Well-structured transition systems everywhere!

Cited in

(66)

• Algorithms for monitoring real-time properties
• Modalities for model checking: Branching time logic strikes back
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Comparing model checking and logical reasoning for real-time systems
• Temporal reasoning through automatic translation of tock-CSP into timed automata
• PuRSUE -- from specification of robotic environments to synthesis of controllers
• Periodicity based decidable classes in a first order timed logic
• A survey on temporal logics for specifying and verifying real-time systems
• Model checking open systems with alternating projection temporal logic
• Model checking of pushdown systems for projection temporal logic
• Model checking restricted sets of timed paths
• Model checking discounted temporal properties
• scientific article; zbMATH DE number 1696823 (Why is no real title available?)
• Parking can get you there faster: model augmentation to speed up real-time model checking
• Bounded model checking for timed automata
• Model checking general linear temporal logic
• Verifying temporal properties in real models
• Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
• scientific article; zbMATH DE number 6117314 (Why is no real title available?)
• Extending CTL with Actions and Real Time
• Timed CTL model checking in Real-Time Maude
• Parametric Timed Model Checking for Guaranteeing Timed Opacity
• Better abstractions for timed automata
• Model Checking Temporal Metric Specifications with Trio2Promela
• Model-Checking Timed ATL for Durational Concurrent Game Structures
• Model Checking Timed Systems with Urgencies
• Timed Temporal Logics for Abstracting Transient States
• scientific article; zbMATH DE number 5368984 (Why is no real title available?)
• Temporal Logic Verification of Lock-Freedom
• Complementary Criteria for Testing Temporal Logic Properties
• scientific article; zbMATH DE number 177234 (Why is no real title available?)
• scientific article; zbMATH DE number 1304997 (Why is no real title available?)
• scientific article; zbMATH DE number 1954132 (Why is no real title available?)
• scientific article; zbMATH DE number 1499083 (Why is no real title available?)
• Template languages for fault monitoring of timed discrete event processes
• A decidable timeout-based extension of linear temporal logic
• Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
• Linear temporal logic symbolic model checking
• scientific article; zbMATH DE number 2102690 (Why is no real title available?)
• scientific article; zbMATH DE number 1418333 (Why is no real title available?)
• scientific article; zbMATH DE number 1439078 (Why is no real title available?)
• An Experimental Spatio-Temporal Model Checker
• Model-Checking Counting Temporal Logics on Flat Structures
• On the Complexity of Temporal-Logic Path Checking
• A menagerie of timed automata
• From Model Checking to a Temporal Proof for Partial Models
• Timed temporal logics
• Model checking real-time systems within unified approach of timed interval temporal logic
• scientific article; zbMATH DE number 6454071 (Why is no real title available?)
• A temporal logic for micro- and macro-step-based real-time systems: foundations and applications
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 6767596 (Why is no real title available?)
• Extending timed automaton and real-time logic to many-valued reasoning
• Counting Models of Linear-Time Temporal Logic
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Timed modal logics for real-time systems. Specification, verification and control
• CONCUR 2005 – Concurrency Theory
• Integrated Formal Methods
• Decidability of model checking with the temporal logic EF
• Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
• Bounded model checking distributed temporal logic
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• Using formal verification to evaluate the execution time of Spark applications
• Coverage metrics for temporal logic model checking

Describes a project that uses

Uses Software

• Kronos
• Uppaal
• HyTech

This page was built for publication: Model-checking timed temporal logics

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