Model-checking timed temporal logics
From MaRDI portal
Publication:4982129
DOI10.1016/J.ENTCS.2009.02.044zbMATH Open1347.68218OpenAlexW1977971680MaRDI QIDQ4982129FDOQ4982129
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
Recommendations
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)
Cites Work
- HyTech: A model checker for hybrid systems
- Uppaal in a nutshell
- A theory of timed automata
- On Expressiveness and Complexity in Real-Time Model Checking
- A really temporal logic
- The benefits of relaxing punctuality
- Title not available (Why is that?)
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Axioms for real-time logics
- Model-checking in dense real-time
- Real-time logics: Complexity and expressiveness
- On Communicating Finite-State Machines
- Foundations of Software Science and Computation Structures
- Symbolic model checking for real-time systems
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- On the decidability and complexity of Metric Temporal Logic over finite words
- Improved undecidability results on weighted timed automata
- Verifying lossy channel systems has nonprimitive recursive complexity.
- Well-structured transition systems everywhere!
- Title not available (Why is that?)
- Title not available (Why is that?)
- Alternating finite automata on \(\omega\)-words
- Title not available (Why is that?)
- Costs Are Expensive!
- Counter-Free Input-Determined Timed Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Alternating timed automata
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Model-Checking One-Clock Priced Timed Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The benefits of relaxing punctuality
- On the Expressiveness of MTL with Past Operators
- Weighted timed automata: model-checking and games
- Foundations of Software Science and Computational Structures
- Title not available (Why is that?)
- CONCUR 2005 – Concurrency Theory
Cited In (63)
- Modalities for model checking: Branching time logic strikes back
- 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
- Title not available (Why is that?)
- Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking
- A survey on temporal logics for specifying and verifying real-time systems
- Timed modal logics for real-time systems. Specification, verification and control
- Model-checking in dense real-time
- Real-time logics: Complexity and expressiveness
- Counting Models of Linear-Time Temporal Logic
- Comparing model checking and logical reasoning for real-time systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Model checking real-time systems within unified approach of timed interval temporal logic
- Periodicity based decidable classes in a first order timed logic
- Complementary Criteria for Testing Temporal Logic Properties
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
- Verifying temporal properties in real models
- Decidability of model checking with the temporal logic EF
- Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
- Integrated Formal Methods
- Model Checking Timed Systems with Urgencies
- Title not available (Why is that?)
- Temporal reasoning through automatic translation of tock-CSP into timed automata
- 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
- Parking can get you there faster: model augmentation to speed up real-time model checking
- Using formal verification to evaluate the execution time of Spark applications
- 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
- Temporal Logic Trees for Model Checking and Control Synthesis of Uncertain Discrete-Time Systems
- Title not available (Why is that?)
- On the Complexity of Temporal-Logic Path Checking
- Model checking general linear temporal logic
- 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
- Title not available (Why is that?)
- Algorithms for monitoring real-time properties
- Bounded model checking for timed automata
- Model checking open systems with alternating projection temporal logic
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
Uses Software
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)
