Towards Bounded Model Checking for the Universal Fragment of TCTL
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1799521
- Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
- The tractability of model checking for LTL: the good, the bad, and the ugly fragments
- The tractability of model-checking for LTL: the good, the bad, and the ugly fragments
- TCTL model checking lower/upper-bound parametric timed automata without invariants
- Abstract model checking of \textsf{tccp} programs
- An experiment on parallel model checking of a CTL fragment
Cited in
(13)- Bounded model checking for knowledge and real time
- Bounded model checking for timed automata
- Bounded model checking for all regular properties
- Checking EMTLK properties of timed interpreted systems via bounded model checking
- scientific article; zbMATH DE number 1799521 (Why is no real title available?)
- A New Approach to Bounded Model Checking for Branching Time Logics
- SAT based bounded model checking with partial order semantics for timed automata
- scientific article; zbMATH DE number 2140441 (Why is no real title available?)
- Bounded semantics
- SAT-based bounded model checking for timed interpreted systems and the RTECTLK properties
- Bounded model checking for the existential fragment of \(\mathrm{TCTL}_{-G}\) and diagonal timed automata
- SAT-based unbounded model checking of timed automata
- Unbounded, fully symbolic model checking of timed automata using Boolean methods.
This page was built for publication: Towards Bounded Model Checking for the Universal Fragment of TCTL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5392295)
