Timed automata relaxation for reachability

DOI10.1007/978-3-030-72016-2_16MaRDI QIDQ2044206zbMATH OpenOpenAlexFDO

Authors Jaroslav Bendík, Ahmet Sencan, Ebru Aydin Gol, I. Černá

Publication date 4 August 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-72016-2_16

zbMATH Keywords

reachabilityrelaxationtimed automata

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1507209
• scientific article; zbMATH DE number 2102690
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 2064232
• scientific article; zbMATH DE number 1962849

Cites work

• A theory of timed automata
• Analysing sanity of requirements for avionics systems
• Bounded Model Checking for Parametric Timed Automata
• Fast, flexible MUS enumeration
• Finding a collection of MUSes incrementally
• scientific article; zbMATH DE number 1701759 (Why is no real title available?)
• scientific article; zbMATH DE number 1796155 (Why is no real title available?)
• scientific article; zbMATH DE number 2102690 (Why is no real title available?)
• Integer Parameter Synthesis for Timed Automata
• Language emptiness of continuous-time parametric timed automata
• LTL parameter synthesis of parametric timed automata
• Minimal sets on propositional formulae. Problems and reductions
• On clock-aware LTL parameter synthesis of timed automata
• On computing minimal independent support and its applications to sampling and counting
• On the optimal reachability problem of weighted timed automata
• Online Enumeration of All Minimal Inductive Validity Cores
• Parametric verification: an introduction
• Recursive online enumeration of all minimal unsatisfiable subsets
• Synthesising robust and optimal parameters for cardiac pacemakers using symbolic and evolutionary computation techniques
• Time-abstracted bisimulation: Implicit specifications and decidability
• Tunable online MUS/MSS enumeration
• Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

Cited in

(14)

• Lazy reachability checking for timed automata using interpolants
• Effective definability of the reachability relation in timed automata
• Remove irrelevant atomic formulas for timed automaton model checking
• Timed recursive state machines: expressiveness and complexity
• Multi-core Reachability for Timed Automata
• Timed automata robustness analysis via model checking
• scientific article; zbMATH DE number 7297846 (Why is no real title available?)
• scientific article; zbMATH DE number 7156375 (Why is no real title available?)
• scientific article; zbMATH DE number 5201490 (Why is no real title available?)
• scientific article; zbMATH DE number 5024617 (Why is no real title available?)
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• Automated repair for timed systems
• Repairing real-time requirements
• Repairing timed automata clock guards through abstraction and testing

This page was built for publication: Timed automata relaxation for reachability

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