Model Checking Real-Time Systems
From MaRDI portal
Publication:3176387
DOI10.1007/978-3-319-10575-8_29zbMath1392.68235OpenAlexW2803623806MaRDI QIDQ3176387
Nicolas Markey, Patricia Bouyer, Joël Ouaknine, Uli Fahrenberg, Kim Guldstrand Larsen, James Worrell
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_29
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (11)
Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Spotlight abstraction in model checking real-time task schedulability ⋮ Temporal Logic and Fair Discrete Systems ⋮ Binary Decision Diagrams ⋮ Combining Model Checking and Deduction ⋮ Graph Games and Reactive Synthesis ⋮ Automated repair for timed systems ⋮ Parameterized model checking of networks of timed automata with Boolean guards ⋮ Dynamic causes for the violation of timed reachability properties ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ A Survey on Analog Models of Computation
Uses Software
Cites Work
- Efficient verification of distributed real-time systems with broadcasting behaviors
- Model-checking in dense real-time
- Real-time logics: Complexity and expressiveness
- Checking timed Büchi automata emptiness efficiently
- Improved undecidability results on weighted timed automata
- Models and formal verification of multiprocessor system-on-chips
- Robust safety of timed automata
- Timed automata and recognizability
- What's decidable about hybrid automata?
- Event-clock automata: a determinizable class of timed automata
- A theory of timed automata
- Symbolic model checking for real-time systems
- Formal methods and software engineering. 5th international conference on formal engineering methods, ICFEM 2003, Singapore, November 5--7, 2003. Proceedings
- Timed automata and additive clock constraints
- PLC-automata: A new class of implementable real-time automata
- Timed tree automata with an application to temporal logic.
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- Linear parametric model checking of timed automata
- Updatable timed automata
- Efficient model-checking of dense-time systems with time-convexity analysis
- On the expressiveness of TPTL and MTL
- Scheduling with timed automata
- Schedulability analysis of fixed-priority systems using timed automata
- Schedulability of asynchronous real-time concurrent objects
- Optimal reachability for multi-priced timed automata
- Formal verification of multitasking applications based on timed automata model
- A partial order semantics approach to the clock explosion problem of timed automata
- A Faster Algorithm for Solving One-Clock Priced Timed Games
- Verification of Asynchronous Circuits using Timed Automata
- Nash Equilibria in Concurrent Priced Games
- Checking timed Büchi automata emptiness on simulation graphs
- Timed automata with observers under energy constraints
- Time-Bounded Verification
- Timed Control with Observation Based and Stuttering Invariant Strategies
- Model Checking One-clock Priced Timed Automata
- Inferring Min and Max Invariants Using Max-Plus Polyhedra
- Timed Concurrent Game Structures
- Semantics and Verification of a Language for Modelling Hardware Architectures
- Infinite Runs in Weighted Timed Automata with Energy Constraints
- Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study
- Undecidability Results for Timed Automata with Silent Transitions
- When Are Timed Automata Determinizable?
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- A really temporal logic
- The benefits of relaxing punctuality
- On the power of non-observable actions in timed automata
- On the synthesis of discrete controllers for timed systems
- The expressive power of clocks
- Robustness in Timed Automata
- What good are digital clocks?
- Parametric real-time reasoning
- Alternating timed automata
- Hybrid Systems: Computation and Control
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- On the decidability and complexity of Metric Temporal Logic over finite words
- Algebraic Methodology and Software Technology
- Almost Optimal Strategies in One Clock Priced Timed Games
- Minimum-Time Reachability in Timed Games
- Fast Directed Model Checking Via Russian Doll Abstraction
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Automata, Languages and Programming
- Lectures on Concurrency and Petri Nets
- Computer Aided Verification
- Automata, Languages and Programming
- Formal Modeling and Analysis of Timed Systems
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- On Interleaving in Timed Automata
- CONCUR 2005 – Concurrency Theory
- Formal Modeling and Analysis of Timed Systems
- Foundations of Software Science and Computation Structures
- CONCUR 2003 - Concurrency Theory
- Computer Aided Verification
- Analysis of timed systems using time-abstracting bisimulations
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Model Checking Real-Time Systems
