Real-Time Model Checking: Algorithms and Complexity

In this talk we describe a new automata-theoretic approach to model checking real-time systems. We show how this approach yields both upper and lower complexity bounds for various decision problems involving timed automata and temporal logics. To put these developments in context we survey some classical results concerning automata, temporal logic and monadic predicate logic over the reals.

Authors

• James Worrell 0001

Keywords

• Automata
• Real time systems
• Logic devices
• Clocks
• Laboratories
• Queueing analysis
• Algorithm design and analysis
• Mathematics
• Model Checking
• Decision Problem
• First-order Logic
• Temporal Logic
• Insertion Errors
• Real-time