Advertisement
Published in:
2012 | OriginalPaper | Chapter
Weighted Probabilistic Equivalence Preserves ω-Regular Properties
Author : Arpit Sharma
Published in: Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.