2012 | OriginalPaper | Buchkapitel
Weighted Probabilistic Equivalence Preserves ω-Regular Properties
verfasst von : Arpit Sharma
Erschienen in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Equivalence relations can be used to reduce the state space of a system model, thereby permitting more efficient analysis. This paper extends the notion of weighted lumpability (WL) defined on continuous-time Markov chains (CTMCs) to the discrete-time setting, i.e., discrete-time Markov chains (DTMCs). We provide a structural definition of weighted probabilistic equivalence (WPE), define the quotient under WPE and prove some elementary properties. We show that
ω
-regular properties are preserved when reducing the state space of a DTMC using WPE. Finally, we show that WPE is
compositional
w.r.t. synchronous parallel composition.