Euclidean model checking: A scalable method for verifying quantitative properties in probabilistic systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We typically represent the global state of a concurrent system as the crossproduct of individual states of its components. This leads to an explosion of potential global states: consider a concurrent system with a thousand actors, each of which may be in one of 5 states. This leads to a possible 5 1000 global states. Obviously, it is not feasible to exhaustively search the state space in such systems. In fact, actors often have an even larger number of states (than say 5), although these states may be abstracted to fewer states.

Original languageEnglish (US)
Title of host publicationAlgebraic Informatics - 5th International Conference, CAI 2013, Proceedings
Pages1-3
Number of pages3
DOIs
StatePublished - 2013
Event5th International Conference on Algebraic Informatics, CAI 2013 - Porquerolles, France
Duration: Sep 3 2013Sep 6 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8080 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th International Conference on Algebraic Informatics, CAI 2013
Country/TerritoryFrance
CityPorquerolles
Period9/3/139/6/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Euclidean model checking: A scalable method for verifying quantitative properties in probabilistic systems'. Together they form a unique fingerprint.

Cite this