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. © 2013 Springer-Verlag.
CITATION STYLE
Agha, G. (2013). Euclidean model checking: A scalable method for verifying quantitative properties in probabilistic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8080 LNCS, pp. 1–3). https://doi.org/10.1007/978-3-642-40663-8_1
Mendeley helps you to discover research relevant for your work.