The Quantitative Linear-Time–Branching-Time Spectrum

Claus Thrane, Uli Fahrenberg, Axel Legay

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

22 Citations (Scopus)

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 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.
Original languageEnglish
Title of host publicationIARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)
EditorsSupratik Chakraborty, Amit Kumar
Number of pages19
Volume13
PublisherSchloss Dagstuhl. Leibniz-Zentrum für Informatik
Publication date2011
Pages103--114
ISBN (Print)978-3-939897-34-7
DOIs
Publication statusPublished - 2011
EventFSTTCS'11 - Mumbai, India
Duration: 12 Dec 201114 Dec 2011

Conference

ConferenceFSTTCS'11
CountryIndia
CityMumbai
Period12/12/201114/12/2011
SeriesLeibniz International Proceedings in Informatics
Volume13
ISSN1868-8969

Keywords

  • Quantitative verification
  • System distance
  • Distance hierarchy
  • Linear time
  • Branching time

Fingerprint

Dive into the research topics of 'The Quantitative Linear-Time–Branching-Time Spectrum'. Together they form a unique fingerprint.

Cite this