Polynomial Interrupt Timed Automata
| Autor: | Claudine Picaronny, Mathieu Sassolas, Serge Haddad, Mohab Safey El Din, Béatrice Bérard |
|---|---|
| Přispěvatelé: | Modélisation et Vérification (MoVe), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Polynomial Systems (PolSys), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Paris 6 (LIP6), Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt |
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Model checking Discrete mathematics Polynomial Formal Languages and Automata Theory (cs.FL) Reachability problem Timed automaton Computer Science - Formal Languages and Automata Theory 0102 computer and information sciences 02 engineering and technology 01 natural sciences Decidability Automaton 010201 computation theory & mathematics Reachability 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] 020201 artificial intelligence & image processing Hybrid automaton Computer Science::Formal Languages and Automata Theory Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319245362 RP The 9th Workshop on Reachability Problems (RP'15) The 9th Workshop on Reachability Problems (RP'15), Sep 2015, Warsaw, Poland. pp.20-32, ⟨10.1007/978-3-319-24537-9_3⟩ |
| DOI: | 10.1007/978-3-319-24537-9_3 |
| Popis: | Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. Here we extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove the decidability of the reachability and model checking of a timed version of CTL by an adaptation of the cylindrical decomposition method for the first-order theory of reals. Compared to previous approaches, our procedure handles parameters and clocks in a unified way. Moreover, we show that PolITA are incomparable with stopwatch automata. Finally additional features are introduced while preserving decidability. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|