On clock-aware LTL parameter synthesis of timed automata

DOI10.1016/j.jlamp.2018.05.004zbMath1395.68164OpenAlexW2804291498MaRDI QIDQ1648651

Ivana Černá, Nikola Beneš, Peter Bezděk, Jiří Barnat

Publication date: 27 June 2018

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2018.05.004

zbMATH Keywords

linear temporal logicparameter synthesisclock-aware linear temporal logicparametric timed automaton

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

Unnamed Item, Timed automata relaxation for reachability

Uses Software

• PPL
• LTL2BA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficient emptiness check for timed Büchi automata
• Checking timed Büchi automata emptiness efficiently
• An automata-theoretic approach to constraint LTL
• Decision problems for lower/upper bound parametric timed automata
• A theory of timed automata
• Linear parametric model checking of timed automata
• Forward analysis of updatable timed automata
• On Clock-Aware LTL Properties of Timed Automata
• Checking timed Büchi automata emptiness on simulation graphs
• Language Emptiness of Continuous-Time Parametric Timed Automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• Checking Timed Büchi Automata Emptiness Using LU-Abstractions
• A really temporal logic
• The benefits of relaxing punctuality
• LTL Parameter Synthesis of Parametric Timed Automata
• Parametric real-time reasoning
• Formal Methods for the Design of Real-Time Systems
• Lectures on Concurrency and Petri Nets
• Analysis of timed systems using time-abstracting bisimulations