A theory of timed automata

DOI10.1016/0304-3975(94)90010-8zbMath0803.68071OpenAlexW2101508170MaRDI QIDQ1322162

David L. Dill, Rajeev Alur

Publication date: 5 May 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90010-8

zbMATH Keywords

verificationundecidabilitytimed automataBüchi automataPSPACE-completebehavior of real-time systemsdeterministic timed Muller automatamodeling of timenondeterministic timed automatatimed language

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (only showing first 100 items - show all)

New Results on Timed Specifications ⋮ Performance Evaluation of Schedulers in a Probabilistic Setting ⋮ Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Probabilistic Real-Time Rewrite Theories and Their Expressive Power ⋮ Statistical Model Checking for Networks of Priced Timed Automata ⋮ Robust Model-Checking of Timed Automata via Pumping in Channel Machines ⋮ Thin and Thick Timed Regular Languages ⋮ Robust Specification of Real Time Components ⋮ Minimum Attention Controller Synthesis for Omega-Regular Objectives ⋮ Exact Incremental Analysis of Timed Automata with an SMT-Solver ⋮ Event Clock Automata: From Theory to Practice ⋮ Composing Stability Proofs for Hybrid Systems ⋮ Modeling for Verification ⋮ Binary Decision Diagrams ⋮ Combining Model Checking and Deduction ⋮ Model Checking Real-Time Systems ⋮ Verification of Hybrid Systems ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ An Abstract Model for Proving Safety of Autonomous Urban Traffic ⋮ Weighted Register Automata and Weighted Logic on Data Words ⋮ Parametric Deadlock-Freeness Checking Timed Automata ⋮ Volume and Entropy of Regular Timed Languages: Discretization Approach ⋮ Concavely-Priced Probabilistic Timed Automata ⋮ Time-Bounded Verification ⋮ Weak Time Petri Nets Strike Back! ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Coinduction in Concurrent Timed Systems ⋮ Tropical Fourier–Motzkin elimination, with an application to real-time verification ⋮ A Logical Characterization of Timed Pushdown Languages ⋮ Quantifying Communication in Synchronized Languages ⋮ Analyzing Oscillatory Behavior with Formal Methods ⋮ Timed Symbolic Dynamics ⋮ Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels ⋮ Improving Search Order for Reachability Testing in Timed Automata ⋮ Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata ⋮ Quantitative Attack Tree Analysis via Priced Timed Automata ⋮ Fluid Model Checking of Timed Properties ⋮ Nested Timed Automata with Frozen Clocks ⋮ Verification and Control of Partially Observable Probabilistic Real-Time Systems ⋮ Deciding Concurrent Planar Monotonic Linear Hybrid Systems ⋮ Bounded Determinization of Timed Automata with Silent Transitions ⋮ Logics for Weighted Timed Pushdown Automata ⋮ Security of Numerical Sensors in Automata ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Relating timed and register automata ⋮ A rewriting framework and logic for activities subject to regulations ⋮ Fault-tolerant continuous flow systems modelling ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Optimal Reachability in Divergent Weighted Timed Games ⋮ Parametric Timed Model Checking for Guaranteeing Timed Opacity ⋮ Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata ⋮ Efficient CTMC Model Checking of Linear Real-Time Objectives ⋮ Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy ⋮ An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP ⋮ Rigorous Simulation-Based Analysis of Linear Hybrid Systems ⋮ Expressiveness of verifiable hierarchical clock systems ⋮ Emptiness and Universality Problems in Timed Automata with Positive Frequency ⋮ On Reachability for Hybrid Automata over Bounded Time ⋮ VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES ⋮ THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Methodologies for Specification of Real-Time Systems Using Timed I/O Automata ⋮ Well (and Better) Quasi-Ordered Transition Systems ⋮ Access Nets: Modeling Access to Physical Spaces ⋮ Verification of Timed-Arc Petri Nets ⋮ Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July/August 2001. ⋮ Timed Automata Can Always Be Made Implementable ⋮ Coarse Abstractions Make Zeno Behaviours Difficult to Detect ⋮ Fixed-Delay Events in Generalized Semi-Markov Processes Revisited ⋮ Formal Models of Timing Attacks on Web Privacy ⋮ Rule Formats for Timed Processes ⋮ Translation from timed Petri nets with intervals on transitions to intervals on places (with urgency) ⋮ Verification of Asynchronous Circuits using Timed Automata ⋮ On Improving Backwards Verification of Timed Automata (Extended Abstract) ⋮ TPAP ⋮ Timed Semantics of Message Sequence Charts Based on Timed Automata ⋮ Modular Synthesis of Timed Circuits using Partial Orders on LPNs ⋮ Parking Can Get You There Faster ⋮ Classes of Timed Automata and the Undecidability of Universality ⋮ Timed CSP = Closed Timed Automata1 ⋮ Proving Safety of Traffic Manoeuvres on Country Roads ⋮ A modular formal semantics for Ptolemy ⋮ Rigorous implementation of real-time systems – from theory to application ⋮ Non-Interference Control Synthesis for Security Timed Automata ⋮ Recent Advances in Real-Time Maude ⋮ Proving Approximate Implementations for Probabilistic I/O Automata ⋮ Time Separation of Events: An Inverse Method ⋮ Keeping Secrets in Resource Aware Components ⋮ Automated formal analysis and verification: an overview ⋮ Towards Deriving Test Sequences by Model Checking ⋮ Automatic Verification of Combined Specifications: An Overview ⋮ On Verification of Linear Occurrence Properties of Real-Time Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata
• Propositional dynamic logic of nonregular programs
• Using branching time temporal logic to synthesize synchronization skeletons
• The complementation problem for Büchi automata with applications to temporal logic
• Complementing deterministic Büchi automata in polynomial time
• Symbolic model checking: \(10^{20}\) states and beyond
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Temporal logic can be more expressive
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Communicating sequential processes
• A Graph-Theoretic Approach for Timing Analysis and its Implementation
• The benefits of relaxing punctuality
• Testing and generating infinite sequences by a finite automaton

This page was built for publication: A theory of timed automata