A survey of timed automata for the development of real-time systems
From MaRDI portal
Publication:394966
DOI10.1016/j.cosrev.2013.05.001zbMath1302.68180OpenAlexW2091661303MaRDI QIDQ394966
Juergen Dingel, Md Tawhid Bin Waez, Karen Rudie
Publication date: 28 January 2014
Published in: Computer Science Review (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.cosrev.2013.05.001
surveytoolsdecision problemsreal-time systemstimed automatasemanticsformal modelsimplementabilitytimed regular languagesvariants
Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items (5)
Model measuring for discrete and hybrid systems ⋮ Equivalence checking and intersection of deterministic timed finite state machines ⋮ Diagnosis of timed patterns for discrete event systems by means of state isolation ⋮ Controller synthesis for dynamic hierarchical real-time plants using timed automata ⋮ Using formal verification to evaluate the execution time of Spark applications
Uses Software
Cites Work
- Model checking weighted integer reset timed automata
- Validation and verification of web services choreographies by using timed automata
- Parametric timing analysis for real-time systems
- Minimum and maximum delay problems in real-time systems
- Model-checking in dense real-time
- Checking timed Büchi automata emptiness efficiently
- Folk theorems on the determinization and minimization of timed automata
- Design and verification of long-running transactions in a timed framework
- Decision problems for lower/upper bound parametric timed automata
- Statecharts: a visual formalism for complex systems
- Complexity of some problems in Petri nets
- Event-clock automata: a determinizable class of timed automata
- A theory of timed automata
- Time-abstracted bisimulation: Implicit specifications and decidability
- Verification in loosely synchronous queue-connected discrete timed automata.
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Formal methods and software engineering. 5th international conference on formal engineering methods, ICFEM 2003, Singapore, November 5--7, 2003. Proceedings
- Past pushdown timed automata and safety verification.
- Computing with membranes
- Timed automata and additive clock constraints
- Automatic verification of real-time systems with discrete probability distributions.
- On probabilistic timed automata.
- HyTech: A model checker for hybrid systems
- Forward analysis of updatable timed automata
- Updatable timed automata
- Timed automata with urgent transitions
- Discrete-time control for rectangular hybrid automata
- Symbolic model checking for probabilistic timed automata
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- On the optimal reachability problem of weighted timed automata
- Optimal reachability for multi-priced timed automata
- Task automata: Schedulability, decidability and undecidability
- Sampled Semantics of Timed Automata
- Checking timed Büchi automata emptiness on simulation graphs
- Quantitative Robustness Analysis of Flat Timed Automata
- Parametric Model Checking with VerICS
- Automatic Verification of Multi-queue Discrete Timed Automata
- Timed Automata Can Always Be Made Implementable
- Robust Specification of Real Time Components
- Concavely-Priced Probabilistic Timed Automata
- Timed regular expressions
- Costs Are Expensive!
- Counter-Free Input-Determined Timed Automata
- Dynamical Properties of Timed Automata Revisited
- Multi-processor Schedulability Analysis of Preemptive Real-Time Tasks with Variable Execution Times
- Symbolic Robustness Analysis of Timed Automata
- Undecidable Problems About Timed Automata
- Distributed Time-Asynchronous Automata
- Robust Model-Checking of Linear-Time Properties in Timed Automata
- Distributed Timed Automata with Independently Evolving Clocks
- Concavely-Priced Timed Automata
- Timed Automata with Integer Resets: Language Inclusion and Expressiveness
- Parametric temporal logic for “model measuring”
- Visibly pushdown languages
- Event-Clock Visibly Pushdown Automata
- Interrupt Timed Automata
- Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions
- Removing All Silent Transitions from Timed Automata
- Alternation
- On the power of bounded concurrency I
- On the power of non-observable actions in timed automata
- On the synthesis of discrete controllers for timed systems
- Recursive Timed Automata
- Superposition-Based Analysis of First-Order Probabilistic Timed Automata
- Modeling Long–Running Transactions with Communicating Hierarchical Timed Automata
- Removing ε-transitions in timed automata
- Timed P Automata
- Parametric real-time reasoning
- Alternating timed automata
- Tools and Algorithms for the Construction and Analysis of Systems
- Real-Time Model-Checking: Parameters everywhere
- On the decidability and complexity of Metric Temporal Logic over finite words
- Computer Aided Verification
- Membrane Computing
- On Continuous Timed Automata with Input-Determined Guards
- Minimum-Time Reachability in Timed Games
- Reachability-Time Games on Timed Automata
- Probabilistic and Topological Semantics for Timed Automata
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- Automated Technology for Verification and Analysis
- Formal Methods for the Design of Real-Time Systems
- Formal Methods for the Design of Real-Time Systems
- A Logical Characterisation of Event Clock Automata
- Lectures on Concurrency and Petri Nets
- Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
- Model-Checking One-Clock Priced Timed Automata
- Formal Methods for Components and Objects
- CONCUR 2005 – Concurrency Theory
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Formal Modeling and Analysis of Timed Systems
- Formal Modeling and Analysis of Timed Systems
- Languages and Tools for Hybrid Systems Design
- Hybrid Systems: Computation and Control
- Weak Alternating Timed Automata
- Analysis of timed systems using time-abstracting bisimulations
- State equivalences for rectangular hybrid automata
- Verifying abstractions of timed systems
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: A survey of timed automata for the development of real-time systems
