Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThe COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains
158
0
0.0
(
0
)
Added by
Nils Jansen
Publication date
2012
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
This report presents the tool COMICS, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command-line version as well as a graphical user interface that allows the user to interactively influence the refinement process of the counterexample.
rate research
Read More
We describe a simple method that can be used to sample the rare fluctuations of discrete-time Markov chains. We focus on the case of Markov chains with well-defined steady-state measures, and derive expressions for the large-deviation rate functions (and upper bounds on such functions) for dynamical quantities extensive in the length of the Markov chain. We illustrate the method using a series of simple examples, and use it to study the fluctuations of a lattice-based model of active matter that can undergo motility-induced phase separation.
Evolution algebras are non-associative algebras. In this work we provide an extension of this class of algebras, in the context of Hilbert spaces, capable to deal with infinite-dimensional spaces. We illustrate the applicability of our approach by discussing a connection with discrete-time Markov chains with countable state space.
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the systems states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.
Continuous-time Markov chains are mathematical models that are used to describe the state-evolution of dynamical systems under stochastic uncertainty, and have found widespread applications in various fields. In order to make these models computationally tractable, they rely on a number of assumptions that may not be realistic for the domain of application; in particular, the ability to provide exact numerical parameter assessments, and the applicability of time-homogeneity and the eponymous Markov property. In this work, we extend these models to imprecise continuous-time Markov chains (ICTMCs), which are a robust generalisation that relaxes these assumptions while remaining computationally tractable. More technically, an ICTMC is a set of precise continuous-time finite-state stochastic processes, and rather than computing expected values of functions, we seek to compute lower expectations, which are tight lower bounds on the expectations that correspond to such a set of precise models. Note that, in contrast to e.g. Bayesian methods, all the elements of such a set are treated on equal grounds; we do not consider a distribution over this set. The first part of this paper develops a formalism for describing continuous-time finite-state stochastic processes that does not require the aforementioned simplifying assumptions. Next, this formalism is used to characterise ICTMCs and to investigate their properties. The concept of lower expectation is then given an alternative operator-theoretic characterisation, by means of a lower transition operator, and the properties of this operator are investigated as well. Finally, we use this lower transition operator to derive tractable algorithms (with polynomial runtime complexity w.r.t. the maximum numerical error) for computing the lower expectation of functions that depend on the state at any finite number of time points.
We consider a generalization of the Ruelle theorem for the case of continuous time problems. We present a result which we believe is important for future use in problems in Mathematical Physics related to $C^*$-Algebras We consider a finite state set $S$ and a stationary continuous time Markov Chain $X_t$, $tgeq 0$, taking values on S. We denote by $Omega$ the set of paths $w$ taking values on S (the elements $w$ are locally constant with left and right limits and are also right continuous on $t$). We consider an infinitesimal generator $L$ and a stationary vector $p_0$. We denote by $P$ the associated probability on ($Omega, {cal B}$). This is the a priori probability. All functions $f$ we consider bellow are in the set ${cal L}^infty (P)$. From the probability $P$ we define a Ruelle operator ${cal L}^t, tgeq 0$, acting on functions $f:Omega to mathbb{R}$ of ${cal L}^infty (P)$. Given $V:Omega to mathbb{R}$, such that is constant in sets of the form ${X_0=c}$, we define a modified Ruelle operator $tilde{{cal L}}_V^t, tgeq 0$. We are able to show the existence of an eigenfunction $u$ and an eigen-probability $ u_V$ on $Omega$ associated to $tilde{{cal L}}^t_V, tgeq 0$. We also show the following property for the probability $ u_V$: for any integrable $gin {cal L}^infty (P)$ and any real and positive $t$ $$ int e^{-int_0^t (V circ Theta_s)(.) ds} [ (tilde{{cal L}}^t_V (g)) circ theta_t ] d u_V = int g d u_V$$ This equation generalize, for the continuous time Markov Chain, a similar one for discrete time systems (and which is quite important for understanding the KMS states of certain $C^*$-algebras).
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
