Interrupt timed automata: verification and expressiveness

DOI10.1007/s10703-011-0140-2zbMath1247.68124arXiv1203.6453OpenAlexW2080957994MaRDI QIDQ453513

Mathieu Sassolas, Béatrice Bérard, Serge Haddad

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1203.6453

zbMATH Keywords

hybrid automatatimed automatamodel checkingdecidability of reachabilityinterruptsmulti-task systemsreal-time properties

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

Timed recursive state machines: expressiveness and complexity ⋮ Polynomial interrupt timed automata: verification and expressiveness ⋮ Revisiting reachability in polynomial interrupt timed automata ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques

Uses Software

• Kronos
• NuSMV
• Uppaal
• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Minimum and maximum delay problems in real-time systems
• Model-checking in dense real-time
• What's decidable about hybrid automata?
• A theory of timed automata
• Symbolic model checking for real-time systems
• Reachability analysis of dynamical systems having piecewise-constant derivatives
• Decidable integration graphs.
• Forward analysis of updatable timed automata
• Algorithmic analysis of polygonal hybrid systems. I: Reachability
• On model-checking timed automata with stopwatch observers
• Task automata: Schedulability, decidability and undecidability
• On Reachability for Hybrid Automata over Bounded Time
• Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets
• Interrupt Timed Automata
• The complexity of propositional linear temporal logics
• Facing up to arrangements: face-count formulas for partitions of space by hyperplanes
• The benefits of relaxing punctuality
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Symbolic reachability computation for families of linear vector fields

This page was built for publication: Interrupt timed automata: verification and expressiveness