DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2011.103

The Quantitative Linear-Time--Branching-Time Spectrum

Authors: Uli Fahrenberg, Axel Legay, and Claus Thrane

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract

We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time--branching-time spectrum to a quantitative setting, parametrized by trace distance. We also provide fixed-point characterizations of all system distances, and we prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting,showing that all system distances are mutually topologically inequivalent.

Cite as

Uli Fahrenberg, Axel Legay, and Claus Thrane. The Quantitative Linear-Time--Branching-Time Spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 103-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fahrenberg_et_al:LIPIcs.FSTTCS.2011.103,
  author =	{Fahrenberg, Uli and Legay, Axel and Thrane, Claus},
  title =	{{The Quantitative Linear-Time--Branching-Time Spectrum}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{103--114},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.103},
  URN =		{urn:nbn:de:0030-drops-33324},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.103},
  annote =	{Keywords: Quantitative verification, System distance, Distance hierarchy, Linear time, Branching time}
}

Document

DOI: 10.4230/DROPS.MEMICS.2009.2345

A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Authors: Kim G. Larsen, Uli Fahrenberg, and Claus Thrane

Published in: OASIcs, Volume 13, Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09) (2009)

Abstract

We extend the usual notion of Kripke Structures with a weighted transition relation, and generalize the usual Boolean satisfaction relation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax, and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.

Cite as

Kim G. Larsen, Uli Fahrenberg, and Claus Thrane. A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic. In Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09). Open Access Series in Informatics (OASIcs), Volume 13, pp. 10-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:OASIcs:2009:DROPS.MEMICS.2009.2345,
  author =	{Larsen, Kim G. and Fahrenberg, Uli and Thrane, Claus},
  title =	{{A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic}},
  booktitle =	{Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'09)},
  pages =	{10--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-15-6},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{13},
  editor =	{Hlinen\'{y}, Petr and Maty\'{a}\v{s}, V\'{a}clav and Vojnar, Tom\'{a}\v{s}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DROPS.MEMICS.2009.2345},
  URN =		{urn:nbn:de:0030-drops-23454},
  doi =		{10.4230/DROPS.MEMICS.2009.2345},
  annote =	{Keywords: Quantitative analysis, Kripke structures, characteristic formulae, bisimulation distance, weighted CTL}
}

Search Results

Documents authored by Thrane, Claus

The Quantitative Linear-Time--Branching-Time Spectrum

Abstract

Cite as

A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message