Interrupt timed automata: verification and expressiveness

DOI10.1007/S10703-011-0140-2MaRDI QIDQ453513zbMATH OpenOpenAlexFDO

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

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 automatamodel checkingtimed automatadecidability of reachabilityinterruptsmulti-task systemsreal-time properties

Mathematics Subject Classification ID

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

Abstract: We introduce the class of Interrupt Timed Automata (ITA), a subclass of hybrid automata well suited to the description of timed multi-task systems with interruptions in a single processor environment. While the reachability problem is undecidable for hybrid automata we show that it is decidable for ITA. More precisely we prove that the untimed language of an ITA is regular, by building a finite automaton as a generalized class graph. We then establish that the reachability problem for ITA is in NEXPTIME and in PTIME when the number of clocks is fixed. To prove the first result, we define a subclass ITA- of ITA, and show that (1) any ITA can be reduced to a language-equivalent automaton in ITA- and (2) the reachability problem in this subclass is in NEXPTIME (without any class graph). In the next step, we investigate the verification of real time properties over ITA. We prove that model checking SCL, a fragment of a timed linear time logic, is undecidable. On the other hand, we give model checking procedures for two fragments of timed branching time logic. We also compare the expressive power of classical timed automata and ITA and prove that the corresponding families of accepted languages are incomparable. The result also holds for languages accepted by controlled real-time automata (CRTA), that extend timed automata. We finally combine ITA with CRTA, in a model which encompasses both classes and show that the reachability problem is still decidable. Additionally we show that the languages of ITA are neither closed under complementation nor under intersection.

Recommendations

• Interrupt Timed Automata
• Polynomial interrupt timed automata: verification and expressiveness
• Interrupt timed automata with auxiliary clocks and parameters
• Polynomial interrupt timed automata
• Revisiting reachability in polynomial interrupt timed automata

Cites work

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

Cited in

(13)

• Corrigendum to: ``Revisiting reachability in polynomial interrupt timed automata
• Revisiting reachability in polynomial interrupt timed automata
• Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
• Parametric Interrupt Timed Automata
• Formal Modeling and Analysis of Timed Systems
• Interrupt Timed Automata
• Lazy reachability checking for timed automata using interpolants
• Interrupt timed automata with auxiliary clocks and parameters
• Polynomial interrupt timed automata
• scientific article; zbMATH DE number 4001464 (Why is no real title available?)
• scientific article; zbMATH DE number 1954132 (Why is no real title available?)
• Polynomial interrupt timed automata: verification and expressiveness
• Timed recursive state machines: expressiveness and complexity

Describes a project that uses

Uses Software

• Kronos
• NuSMV
• Uppaal
• CESAR

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q453513)