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

By Gul Agha. In Algebraic Informatics - 5th International Conference, CAI 2013, Porquerolles, France, September 3-6, 2013. Proceedings, volume 8080 of Lecture Notes in Computer Science, 1–3. Springer, 2013.

DOI:

10.1007/978-3-642-40663-8_1

Publisher Link:

https://doi.org/10.1007/978-3-642-40663-8_1

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 51000 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.

BibTeX

@inproceedings{conf/cai/Agha13,
    author = "Agha, Gul",
    editor = "Muntean, Traian and Poulakis, Dimitrios and Rolland,
              Robert",
    title = "Euclidean Model Checking: {A} Scalable Method for
             Verifying Quantitative Properties in Probabilistic Systems",
    biburl = "https://dblp.org/rec/bib/conf/cai/Agha13",
    booktitle = "Algebraic Informatics - 5th International
                 Conference, {CAI} 2013, Porquerolles, France, September 3-6,
                 2013. Proceedings",
    crossref = "conf/cai/2013",
    doi = "10.1007/978-3-642-40663-8\_1",
    pages = "1--3",
    timestamp = "Thu, 15 Jun 2017 21:34:06 +0200",
    url = "https://doi.org/10.1007/978-3-642-40663-8\_1",
    year = "2013",
}

@proceedings{conf/cai/2013,
    editor = "Muntean, Traian and Poulakis, Dimitrios and Rolland,
              Robert",
    title = "Algebraic Informatics - 5th International Conference,
             {CAI} 2013, Porquerolles, France, September 3-6, 2013.
             Proceedings",
    biburl = "https://dblp.org/rec/bib/conf/cai/2013",
    doi = "10.1007/978-3-642-40663-8",
    isbn = "978-3-642-40662-1",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    timestamp = "Thu, 15 Jun 2017 21:34:06 +0200",
    url = "https://doi.org/10.1007/978-3-642-40663-8",
    volume = "8080",
    year = "2013",
}