Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOnline Monitoring $omega$-Regular Properties in Unknown Markov Chains
61
0
0.0
(
0
)
Added by
Jan K\\v{r}et\\'insk\\'y
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We study runtime monitoring of $omega$-regular properties. We consider a simple setting in which a run of an unknown finite-state Markov chain $mathcal M$ is monitored against a fixed but arbitrary $omega$-regular specification $varphi$. The purpose of monitoring is to keep aborting runs that are unlikely to satisfy the specification until $mathcal M$ executes a correct run. We design controllers for the reset action that (assuming that $varphi$ has positive probability) satisfy the following property w.p.1: the number of resets is finite, and the run executed by $mathcal M$ after the last reset satisfies $varphi$.
rate research
Read More
In this paper, we address the approximate minimization problem of Markov Chains (MCs) from a behavioral metric-based perspective. Specifically, given a finite MC and a positive integer k, we are looking for an MC with at most k states having minimal distance to the original. The metric considered in this work is the bisimilarity distance of Desharnais et al.. For this metric we show that (1) optimal approximations always exist; (2) the problem has a bilinear program characterization; and (3) prove that its threshold problem is in PSPACE and NP-hard. In addition to the bilinear program solution, we present an approach inspired by expectation maximization techniques for computing suboptimal solutions to the problem. Experiments suggest that our method gives a practical approach that outperforms the bilinear program implementation run on state-of-the-art bilinear solvers.
Dealing with finite Markov chains in discrete time, the focus often lies on convergence behavior and one tries to make different copies of the chain meet as fast as possible and then stick together. There is, however, a very peculiar kind of discrete finite Markov chain, for which two copies started in different states can be coupled to meet almost surely in finite time, yet their distributions keep a total variation distance bounded away from 0, even in the limit as time goes off to infinity. We show that the supremum of total variation distance kept in this context is $frac12$.
We review recent results on the metastable behavior of continuous-time Markov chains derived through the characterization of Markov chains as unique solutions of martingale problems.
We introduce the space of virtual Markov chains (VMCs) as a projective limit of the spaces of all finite state space Markov chains (MCs), in the same way that the space of virtual permutations is the projective limit of the spaces of all permutations of finite sets. We introduce the notions of virtual initial distribution (VID) and a virtual transition matrix (VTM), and we show that the law of any VMC is uniquely characterized by a pair of a VID and VTM which have to satisfy a certain compatibility condition. Lastly, we study various properties of compact convex sets associated to the theory of VMCs, including that the Birkhoff-von Neumann theorem fails in the virtual setting.
This paper introduces two mechanisms for computing over-approximations of sets of reachable states, with the aim of ensuring termination of state-space exploration. The first mechanism consists in over-approximating the automata representing reachable sets by merging some of their states with respect to simple syntactic criteria, or a combination of such criteria. The second approximation mechanism consists in manipulating an auxiliary automaton when applying a transducer representing the transition relation to an automaton encoding the initial states. In addition, for the second mechanism we propose a new approach to refine the approximations depending on a property of interest. The proposals are evaluated on examples of mutual exclusion protocols.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
