On clock-aware LTL parameter synthesis of timed automata

J 2018

On clock-aware LTL parameter synthesis of timed automata

BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ a Jiří BARNAT

Základní údaje

Originální název

On clock-aware LTL parameter synthesis of timed automata

Autoři

BEZDĚK, Peter (703 Slovensko, domácí), Nikola BENEŠ (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, garant, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Journal of Logical and Algebraic Methods in Programming, ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH, Elsevier, 2018, 2352-2208

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL URL URL

Impakt faktor

Impact factor: 0.632

Kód RIV

RIV/00216224:14330/18:00101069

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1016/j.jlamp.2018.05.004

UT WoS

000437073800005

Klíčová slova anglicky

Parameter Synthesis; Parametric Timed Automata; Linear Temporal Logic

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 10. 2020 09:22, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique.

Návaznosti

GA18-02177S, projekt VaV

Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Citovat

BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ a Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. Journal of Logical and Algebraic Methods in Programming. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, 2018, roč. 99, Oct, s. 114-142. ISSN 2352-2208. Dostupné z: https://dx.doi.org/10.1016/j.jlamp.2018.05.004.

@article{1423692,
   author = {Bezděk, Peter and Beneš, Nikola and Černá, Ivana and Barnat, Jiří},
   article_location = {ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH},
   article_number = {Oct},
   doi = {http://dx.doi.org/10.1016/j.jlamp.2018.05.004},
   keywords = {Parameter Synthesis; Parametric Timed Automata; Linear Temporal Logic},
   language = {eng},
   issn = {2352-2208},
   journal = {Journal of Logical and Algebraic Methods in Programming},
   title = {On clock-aware LTL parameter synthesis of timed automata},
   url = {https://www.sciencedirect.com/science/article/pii/S2352220817300354},
   volume = {99},
   year = {2018}
}

TY  - JOUR
ID  - 1423692
AU  - Bezděk, Peter - Beneš, Nikola - Černá, Ivana - Barnat, Jiří
PY  - 2018
TI  - On clock-aware LTL parameter synthesis of timed automata
JF  - Journal of Logical and Algebraic Methods in Programming
VL  - 99
IS  - Oct
SP  - 114-142
EP  - 114-142
PB  - Elsevier
SN  - 23522208
KW  - Parameter Synthesis
KW  - Parametric Timed Automata
KW  - Linear Temporal Logic
UR  - https://www.sciencedirect.com/science/article/pii/S2352220817300354
L2  - https://www.sciencedirect.com/science/article/pii/S2352220817300354
N2  - The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. The investigated bounded integer parameter synthesis problem could be solved using an explicit enumeration of all possible parameter valuations. We propose an alternative symbolic zone-based method for this problem which can result in a faster computation. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata. In order to simplify the explanation of our method, we first introduce a parameter synthesis algorithm for timed automata, then we describe method for checking Clock-Aware LTL properties of timed automata and finally we combine these two methods together to provide general parameter synthesis algorithm for Clock-Aware LTL properties. To demonstrate the usefulness of our approach, we provide experimental evaluation and compare the proposed method with the explicit enumeration technique.
ER  -

BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ a Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. \textit{Journal of Logical and Algebraic Methods in Programming}. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, 2018, roč.~99, Oct, s.~114-142. ISSN~2352-2208. Dostupné z: https://dx.doi.org/10.1016/j.jlamp.2018.05.004.

Podrobný výpis o publikaci