Parametric Interrupt Timed Automata

被引：0

作者：

Berard, Beatrice ^{[1
]}

Haddad, Serge ^{[2
]}

Jovanovic, Aleksandra ^{[3
]}

Lime, Didier ^{[3
]}

机构：

[1] Univ Paris 06, CNRS, MoVe LIP6, Paris, France

[2] ENS Cachan, LSV, CNRS, INRIA, Cachan, France

[3] LUNAM Univ, Ecole Cent Nantes, IRCCyN, CNRS, Nantes, France

来源：

REACHABILITY PROBLEMS | 2013年 / 8169卷

关键词：

VERIFICATION;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Parametric reasoning is particularly relevant for timed models, but very often leads to undecidability of reachability problems. We propose a parametrised version of Interrupt Timed Automata (an expressive model incomparable to Timed Automata), where polynomials of parameters can occur in guards and updates. We prove that different reachability problems, including robust reachability, are decidable for this model, and we give complexity upper bounds for a fixed or variable number of clocks and parameters.

引用

页码：59 / 69

页数：11

共 50 条

[1] Interrupt Timed Automata
Berard, Beatrice
Haddad, Serge
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2009, 5504 : 197 - +
[2] Interrupt Timed Automata: verification and expressiveness
Béatrice Bérard
Serge Haddad
Mathieu Sassolas
Formal Methods in System Design, 2012, 40 : 41 - 87
[3] Interrupt Timed Automata: verification and expressiveness
Berard, Beatrice
Haddad, Serge
Sassolas, Mathieu
FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) : 41 - 87
[4] Revisiting reachability in Polynomial Interrupt Timed Automata
Bérard, Béatrice
Haddad, Serge
Information Processing Letters, 2022, 174
[5] Polynomial interrupt timed automata: Verification and expressiveness
Berard, B.
Haddad, S.
Picaronny, C.
El Din, M. Safey
Sassolas, M.
INFORMATION AND COMPUTATION, 2021, 277
[6] Interrupt Timed Automata with Auxiliary Clocks and Parameters
Berard, Beatrice
Haddad, Serge
Jovanovic, Aleksandra
Lime, Didier
FUNDAMENTA INFORMATICAE, 2016, 143 (3-4) : 235 - 259
[7] Revisiting reachability in Polynomial Interrupt Timed Automata
Berard, Beatrice
Haddad, Serge
INFORMATION PROCESSING LETTERS, 2022, 174
[8] Parametric Updates in Parametric Timed Automata
Andre, Etienne
Lime, Didier
Ramparison, Mathias
FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS (FORTE 2019), 2019, 11535 : 39 - 56
[9] PARAMETRIC UPDATES IN PARAMETRIC TIMED AUTOMATA
Andre, Etienne
Lime, Didier
Ramparison, Mathias
LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 1 - 13
[10] On the Expressiveness of Parametric Timed Automata
Andre, Etienne
Lime, Didier
Roux, Olivier H.
FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 19 - 34

← 1 2 3 4 5 →