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

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) 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

• 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?)
• 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
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• 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
• HyTech: A model checker for hybrid systems
• Improved undecidability results on weighted timed automata
• Model-Checking One-Clock Priced Timed Automata
• Model-checking in dense real-time
• On Communicating Finite-State Machines
• On Expressiveness and Complexity in Real-Time Model Checking
• On the Expressiveness of MTL with Past Operators
• On the decidability and complexity of Metric Temporal Logic over finite words
• 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

(63)

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

Describes a project that uses

Uses Software

• Uppaal
• HyTech
• Kronos

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)