DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2019.13

Minimisation of Models Satisfying CTL Formulas

Authors: Serenella Cerrito, Amélie David, and Valentin Goranko

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract

We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.

Cite as

Serenella Cerrito, Amélie David, and Valentin Goranko. Minimisation of Models Satisfying CTL Formulas. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{cerrito_et_al:LIPIcs.TIME.2019.13,
  author =	{Cerrito, Serenella and David, Am\'{e}lie and Goranko, Valentin},
  title =	{{Minimisation of Models Satisfying CTL Formulas}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.13},
  URN =		{urn:nbn:de:0030-drops-113718},
  doi =		{10.4230/LIPIcs.TIME.2019.13},
  annote =	{Keywords: CTL, model minimisation, bisimulation reduction, tableaux-based reduction}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2016.28

On the Expressiveness of QCTL

Authors: Amélie David, Francois Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract

QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).

Cite as

Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{david_et_al:LIPIcs.CONCUR.2016.28,
  author =	{David, Am\'{e}lie and Laroussinie, Francois and Markey, Nicolas},
  title =	{{On the Expressiveness of QCTL}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.28},
  URN =		{urn:nbn:de:0030-drops-61643},
  doi =		{10.4230/LIPIcs.CONCUR.2016.28},
  annote =	{Keywords: Specification, Verification, Temporal Logic, Expressiveness, Tree automata}
}

Search Results

Documents authored by David, Amélie

Minimisation of Models Satisfying CTL Formulas

Abstract

Cite as

On the Expressiveness of QCTL

Abstract

Cite as

Thanks for your feedback!

Could not send message