Minimisation of models satisfying CTL formulas

DOI10.4230/LIPICS.TIME.2019.13MaRDI QIDQ6487557zbMATH OpenFDO

Authors

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.TIME.2019.13

zbMATH Keywords

bisimulation reductionCTLmodel minimisationtableaux-based reduction

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Minimisation of \(\mathrm{ATL}^*\) models
• Quirky quantifiers: optimal models and complexity of computation tree logic
• scientific article; zbMATH DE number 2090074
• CTL update of Kripke models through protections
• Minimization of probabilistic models of programs

Cited in

(8)

• Minimisation of \(\mathrm{ATL}^*\) models
• Counterexample-preserving reduction for symbolic model checking
• CTL update of Kripke models through protections
• scientific article; zbMATH DE number 1614696 (Why is no real title available?)
• Coinduction-based solution for minimization of Kripke structures
• Nondeterministic update of CTL models by preserving satisfaction through protections
• Fast, flexible, and minimal CTL synthesis via SMT
• Minimization of probabilistic models of programs

This page was built for publication: Minimisation of models satisfying CTL formulas

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