Approximation Metrics Based on Probabilistic Bisimulations for General State-Space Markov Processes: A Survey
---
paper_title: Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

paper_content:

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experiments or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of epsi-simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines epsi-(bi)simulation. Of course, for all the notions defined, letting epsi = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens in fully probabilistic systems when epsi = 0, two-way e-simulation for epsi > 0 is not equal to epsi-bisimulation. Next we give a polynomial time algorithm to compute a naturally derived metric: distance between states s and t is defined as the smallest epsi such that s and t are epsi-equivalent. This is the first polynomial algorithm for a non-discounted metric. Finally we show that most of these notions can be extended to deal with probabilistic systems that allow non-determinism as well.
---
paper_title: Weak Bisimulation for Fully Probabilistic Processes

paper_content:

Bisimulations that abstract from internal computation have proven to be useful for verification of compositionally defined transition systems. In the literature of probabilistic extensions of such transition systems, similar bisimulations are rare. In this paper, we introduce weak and branching bisimulation for fully probabilistic systems, transition systems where nondeterministic branching is replaced by probabilistic branching. In contrast to the nondeterministic case, both relations coincide. We give an algorithm to decide weak (and branching) bisimulation with a time complexity cubic in the number of states of the fully probabilistic system. This meets the worst case complexity for deciding branching bisimulation in the nondeterministic case. In addition, the relation is shown to be a congruence with respect to the operators of PLSCCS, a lazy synchronous probabilistic variant of CCS. We illustrate that due to these properties, weak bisimulation provides all the crucial ingredients for mechanised compositional veri�cation of probabilistic transition systems.
---
paper_title: Principles of Model Checking

paper_content:

Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.
---
paper_title: Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems

paper_content:

Switched systems constitute an important modeling paradigm faithfully describing many engineering systems in which software interacts with the physical world. Despite considerable progress on stability and stabilization of switched systems, the constant evolution of technology demands that we make similar progress with respect to different, and perhaps more complex, objectives. This paper describes one particular approach to address these different objectives based on the construction of approximately equivalent (bisimilar) symbolic models for switched systems. The main contribution of this paper consists in showing that under standard assumptions ensuring incremental stability of a switched system (i.e., existence of a common Lyapunov function, or multiple Lyapunov functions with dwell time), it is possible to construct a finite symbolic model that is approximately bisimilar to the original switched system with a precision that can be chosen a priori. To support the computational merits of the proposed approach, we use symbolic models to synthesize controllers for two examples of switched systems, including the boost dc-dc converter.
---
paper_title: Exact and Ordinary Lumpability in Finite Markov Chains

paper_content:

Exact and ordinary lumpability in finite Markov chains is considered. Both concepts naturally define an aggregation of the Markov chain yielding an aggregated chain that allows the exact determination of several stationary and transient results for the original chain. We show which quantities can be determined without an error from the aggregated process and describe methods to calculate bounds on the remaining results. Furthermore, the concept of lumpability is extended to near
---
paper_title: Probabilistic Simulations for Probabilistic Processes

paper_content:

Several probabilistic simulation relations for probabilistic systems are defined and evaluated according to two criteria: compositionality and preservation of “interesting” properties. Here, the interesting properties of a system are identified with those that are expressible in an untimed version of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson. The definitions are made, and the evaluations carried out, in terms of a general labeled transition system model for concurrent probabilistic computation. The results cover weak simulations, which abstract from internal computation, as well as strong simulations, which do not.
---
paper_title: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes

paper_content:

In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes—called continuous stochastic logic (henceforth CSL)—against continuous-time Markov chains—henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question—does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is “yes”. In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded.
---
paper_title: O-Minimal Hybrid Systems

paper_content:

An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist.
---
paper_title: Bisimulation for probabilistic transition systems: a coalgebraic approach

paper_content:

Abstract The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendler in terms of a set functor, which associates to a set its collection of simple probability distributions. This coalgebraic formulation makes it possible to generalize the concepts of discrete probabilistic transition system and probabilistic bisimulation to a continuous setting involving Borel probability measures. A functor ℳ 1 is introduced that yields for a metric space its collection of Borel probability measures. Under reasonable conditions, this functor exactly captures generalized probabilistic bisimilarity. Application of the final coalgebra paradigm to a functor based on ℳ 1 then yields an internally fully abstract semantical domain with respect to probabilistic bisimulation, which is therefore well suited for the interpretation of probabilistic specification and stochastic programming concepts.
---
paper_title: Approximately bisimilar symbolic models for nonlinear control systems

paper_content:

Control systems are usually modeled by differential equations describing how physical phenomena can be influenced by certain control parameters or inputs. Although these models are very powerful when dealing with physical phenomena, they are less suitable to describe software and hardware interfacing the physical world. For this reason there is a growing interest in describing control systems through symbolic models that are abstract descriptions of the continuous dynamics, where each "symbol" corresponds to an "aggregate" of states in the continuous model. Since these symbolic models are of the same nature of the models used in computer science to describe software and hardware, they provide a unified language to study problems of control in which software and hardware interact with the physical world. Furthermore the use of symbolic models enables one to leverage techniques from supervisory control and algorithms from game theory for controller synthesis purposes. In this paper we show that every incrementally globally asymptotically stable nonlinear control system is approximately equivalent (bisimilar) to a symbolic model. The approximation error is a design parameter in the construction of the symbolic model and can be rendered as small as desired. Furthermore if the state space of the control system is bounded the obtained symbolic model is finite. For digital control systems, and under the stronger assumption of incremental input-to-state stability, symbolic models can be constructed through a suitable quantization of the inputs.
---
paper_title: Bisimulation for Labelled Markov Processes

paper_content:

In this paper we introduce a new class of labelled transition systems - Labelled Markov Processes - and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou denition for discrete systems, is indeed an equivalence relation. This turns out to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.
---
paper_title: HYTECH: A Model Checker for Hybrid Systems

paper_content:

A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.
---
paper_title: Bisimulation for general stochastic hybrid systems

paper_content:

In this paper we define a bisimulation concept for some very general models for stochastic hybrid systems (general stochastic hybrid systems). The definition of bisimulation builds on the ideas of Edalat and of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result is that this bisimulation for GSHS is indeed an equivalence relation. The secondary result is that this bisimulation relation for the stochastic hybrid system models used in this paper implies the same kind of bisimulation for their continuous parts and respectively for their jumping structures.
---
paper_title: Bisimulation for Communicating Piecewise Deterministic Markov Processes (CPDPs)

paper_content:

CPDPs (Communicating Piecewise Deterministic Markov Processes) can be used for compositional specification of systems from the class of stochastic hybrid processes formed by PDPs (Piecewise Deterministic Markov Processes). We define CPDPs and the composition of CPDPs, and prove that the class of CPDPs is closed under composition. Then we introduce a notion of bisimulation for PDPs and CPDPs and we prove that bisimilar PDPs as well as bisimilar CPDPs have equal stochastic behavior. Finally, as main result, we prove the congruence property that, for a composite CPDP, substituting components by different but bisimilar components results in a CPDP that is bisimilar to the original composite CPDP (and therefore has equal stochastic behavior). © Springer-Verlag Berlin Heidelberg 2005.
---
paper_title: Metrics for Markov Decision Processes with Infinite State Spaces

paper_content:

We present metrics for measuring state similarity in Markov decision processes (MDPs) with infinitely many states, including MDPs with continuous state spaces. Such metrics provide a stable quantitative analogue of the notion of bisimulation for MDPs, and are suitable for use in MDP approximation. We show that the optimal value function associated with a discounted infinite horizon planning task varies continuously with respect to our metric distances.
---
paper_title: Metrics for Finite Markov Decision Processes

paper_content:

We present metrics for measuring the similarity of states in a finite Markov decision process (MDP). The formulation of our metrics is based on the notion of bisimulation for MDPs, with an aim towards solving discounted infinite horizon reinforcement learning tasks. Such metrics can be used to aggregate states, as well as to better structure other value function approximators (e.g., memory-based or nearest-neighbor approximators). We provide bounds that relate our metric distances to the optimal values of states in the given MDP.
---
paper_title: Approximation Metrics for Discrete and Continuous Systems

paper_content:

Established system relationships for discrete systems, such as language inclusion, simulation, and bisimulation, require system observations to be identical. When interacting with the physical world, modeled by continuous or hybrid systems, exact relationships are restrictive and not robust. In this paper, we develop the first framework of system approximation that applies to both discrete and continuous systems by developing notions of approximate language inclusion, approximate simulation, and approximate bisimulation relations. We define a hierarchy of approximation pseudo-metrics between two systems that quantify the quality of the approximation, and capture the established exact relationships as zero sections. Our approximation framework is compositional for a synchronous composition operator. Algorithms are developed for computing the proposed pseudo-metrics, both exactly and approximately. The exact algorithms require the generalization of the fixed point algorithms for computing simulation and bisimulation relations, or dually, the solution of a static game whose cost is the so-called branching distance between the systems. Approximations for the pseudo-metrics can be obtained by considering Lyapunov-like functions called simulation and bisimulation functions. We illustrate our approximation framework in reducing the complexity of safety verification problems for both deterministic and nondeterministic continuous systems
---
paper_title: A theory of timed automata

paper_content:

Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. We propose timed (j&e) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Biichi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (II i-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.
---
paper_title: Bisimilar linear systems

paper_content:

The notion of bisimulation in theoretical computer science is one of the main complexity reduction methods for the analysis and synthesis of labeled transition systems. Bisimulations are special quotients of the state space that preserve many important properties expressible in temporal logics, and, in particular, reachability. In this paper, the framework of bisimilar transition systems is applied to various transition systems that are generated by linear control systems. Given a discrete-time or continuous-time linear system, and a finite observation map, we characterize linear quotient maps that result in quotient transition systems that are bisimilar to the original system. Interestingly, the characterizations for discrete-time systems are more restrictive than for continuous-time systems, due to the existence of an atomic time step. We show that computing the coarsest bisimulation, which results in maximum complexity reduction, corresponds to computing the maximal controlled or reachability invariant subspace inside the kernel of the observations map. These results establish strong connections between complexity reduction concepts in control theory and computer science.
---
paper_title: Equivalence notions and model minimization in Markov decision processes

paper_content:

Many stochastic planning problems can be represented using Markov Decision Processes (MDPs). A difficulty with using these MDP representations is that the common algorithms for solving them run in time polynomial in the size of the state space, where this size is extremely large for most real-world planning problems of interest. Recent AI research has addressed this problem by representing the MDP in a factored form. Factored MDPs, however, are not amenable to traditional solution methods that call for an explicit enumeration of the state space. One familiar way to solve MDP problems with very large state spaces is to form a reduced (or aggregated) MDP with the same properties as the original MDP by combining "equivalent" states. In this paper, we discuss applying this approach to solving factored MDP problems--we avoid enumerating the state space by describing large blocks of "equivalent" states in factored form, with the block descriptions being inferred directly from the original factored representation. The resulting reduced MDP may have exponentially fewer states than the original factored MDP, and can then be solved using traditional methods. The reduced MDP found depends on the notion of equivalence between states used in the aggregation. The notion of equivalence chosen will be fundamental in designing and analyzing algorithms for reducing MDPs. Optimally, these algorithms will be able to find the smallest possible reduced MDP for any given input MDP and notion of equivalence (i.e., find the "minimal model" for the input MDP). Unfortunately, the classic notion of state equivalence from non-deterministic finite state machines generalized to MDPs does not prove useful. We present here a notion of equivalence that is based upon the notion of bisimulation from the literature on concurrent processes. Our generalization of bisimulation to stochastic processes yields a non-trivial notion of state equivalence that guarantees the optimal policy for the reduced model immediately induces a corresponding Optimal policy for the original model. With this notion of state equivalence, we design and analyze an algorithm that minimizes arbitrary factored MDPs and compare this method analytically to previous algorithms for solving factored MDPs. We show that previous approaches implicitly derive equivalence relations that we define here.
---
paper_title: Specification and refinement of probabilistic processes

paper_content:

A formalism for specifying probabilistic transition systems, which constitute a basic semantic model for description and analysis of, e.g. reliability aspects of concurrent and distributed systems, is presented. The formalism itself is based on transition systems. Roughly a specification has the form of a transition system in which transitions are labeled by sets of allowed probabilities. A satisfaction relation between processes and specifications that generalizes probabilistic bisimulation equivalence is defined. It is shown that it is analogous to the extension from processes to modal transition systems given by K. Larsen and B. Thomsen (1988). Another weaker criterion views a specification as defining a set of probabilistic processes; refinement is then simply containment between sets of processes. A complete method for verifying containment between specifications, which extends methods for deciding containment between specifications, which extends methods for deciding containment between finite automata or tree acceptors, is presented. >
---
paper_title: Concurrency and Automata on Infinite Sequences

paper_content:

The paper is concerned with ways in which fair concurrency can be modeled using notations for omega-regular languages - languages containing infinite sequences, whose recognizers a.re modified forms of Buchi or Muller-McNaughton automata. There are characterization of these languages in terms of recursion equation sets which involve both minimal and maximal fix point operators. The class of ω-regular languages is closed under a fair concurrency operator. A general method for proving/deciding equivalences between such languages is obtained, derived from Milner's notion of "simulation".
---
paper_title: The metric analogue of weak bisimulation for probabilistic processes

paper_content:

We observe that equivalence is not a robust concept in the presence of numerical information - such as probabilities-in the model. We develop a metric analogue of weak bisimulation in the spirit of our earlier work on metric analogues for strong bisimulation. We give a fixed point characterization of the metric. This makes available conductive reasoning principles and allows us to prove metric analogues of the usual algebraic laws for process combinators. We also show that quantitative properties of interest are continuous with respect to the metric, which says that if two processes are close in the metric then observable quantitative properties of interest are indeed close. As an important example of this we show that nearby processes have nearby channel capacities - a quantitative measure of their propensity to leak information.
---
paper_title: Abstraction in Probabilistic Process AlgebraS

paper_content:

Process algebras with abstraction have been widely used for the specification and verification of non-probabilistic concurrent systems. The main strategy in these algebras is introducing a constant, denoting an internal action, and a set of fairness rules. Following the same approach, in this paper we propose a fully probabilistic process algebra with abstraction which contains a set of verification rules as counterparts of the fairness rules in standard ACP-like process algebras with abstraction. Having probabilities present and employing the results from Markov chain analysis, these rules are expressible in a very intuitive way. In addition to this algebraic approach, we introduce a new version of probabilistic branching bisimulation for the alternating model of probabilistic systems. Different from other approaches, this bisimulation relation requires the same probability measure only for specific related processes called entries. We claim this definition corresponds better with intuition. Moreover, the fairness rules are sound in the model based on this bisimulation. Finally, we present an algorithm to decide our branching bisimulation with a polynomial-time complexity in the number of the states of the probabilistic graph.
---
paper_title: Bisimilar control affine systems

paper_content:

The notion of bisimulation plays a very important role in theoretical computer science where it provides several notions of equivalence between models of computation. These equivalences are in turn used to simplify analysis and synthesis for these models. In system theory, a similar notion is also of interest in order to develop modular analysis and design tools for purely continuous or hybrid control systems. We introduce two notions of bisimulation for nonlinear systems. We present a differential-algebraic characterization of these notions and show that bisimilar systems of different dimensions are obtained by factoring out certain invariant distributions. Furthermore, we also show that all bisimilar systems of different dimension are of this form.
---
paper_title: Comparative Branching-Time Semantics for Markov Chains

paper_content:

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation preorders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous-and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: On infinite-horizon probabilistic properties and stochastic bisimulation functions

paper_content:

This work investigates infinite-horizon properties over discrete-time stochastic models with continuous state spaces. The focus is on understanding how the structural features of a model (e.g., the presence of absorbing sets) affect the values of these properties and relate to their uniqueness. Furthermore, we argue that the investigation of these features can lead to approximation bounds for the value of such properties, as well as to improvements on their computation. The article employs the presented results to find a stochastic bisimulation function of two processes.
---
paper_title: Approximate abstractions of stochastic systems: A randomized method

paper_content:

This work introduces a randomized method for the design of an approximate abstraction of a stochastic system and the assessment of its quality. The proposed approach relies on the formulation of the problem as a semi-infinite chance-constrained optimization program and on its solution via randomization. The method has quite general applicability, since it only requires to be able to run multiple executions of the candidate abstract model and of the original system and to compute their distance. Two variants of the notion of distance are considered in view of a possible use of the approximate abstraction for probabilistic safety verification. The approach is tested on a numerical example.
---
paper_title: A contractivity approach for probabilistic bisimulations of diffusion processes

paper_content:

This work is concerned with the problem of characterizing and computing probabilistic bisimulations of diffusion processes. A probabilistic bisimulation relation between two such processes is defined through a bisimulation function, which induces an approximation metric on the expectation of the (squared norm of the) distance between the two processes. We introduce sufficient conditions for the existence of a bisimulation function, based on the use of contractivity analysis for probabilistic systems. Furthermore, we show that the notion of stochastic contractivity is related to a probabilistic version of the concept of incremental stability. This relationship leads to a procedure that constructs a discrete approximation of a diffusion process. The procedure is based on the discretization of space and time. Given a diffusion process, we raise sufficient conditions for the existence of such an approximation, and show that it is probabilistically bisimilar to the original process, up to a certain approximation precision.
---
paper_title: Approximate Abstractions of Stochastic Hybrid Systems

paper_content:

We present a constructive procedure for obtaining a finite approximate abstraction of a discrete-time stochastic hybrid system. The procedure consists of a partition of the state space of the system and depends on a controllable parameter. Given proper continuity assumptions on the model, the approximation errors introduced by the abstraction procedure are explicitly computed and it is shown that they can be tuned through the parameter of the partition. The abstraction is interpreted as a Markov set-Chain. We show that the enforcement of certain ergodic properties on the stochastic hybrid model implies the existence of a finite abstraction with finite error in time over the concrete model, and allows introducing a finite-time algorithm that computes the abstraction.
---
paper_title: Approximations of Stochastic Hybrid Systems

paper_content:

This paper develops a notion of approximation for a class of stochastic hybrid systems that includes, as special cases, both jump linear stochastic systems and linear stochastic hybrid automata. Our approximation framework is based on the recently developed notion of the so-called stochastic simulation functions. These Lyapunov-like functions can be used to rigorously quantify the distance or error between a system and its approximate abstraction. For the class of jump linear stochastic systems and linear stochastic hybrid automata, we show that the computation of stochastic simulation functions can be cast as a tractable linear matrix inequality problem. This enables us to compute the modeling error incurred by abstracting some of the continuous dynamics, or by neglecting the influence of stochastic noise, or even the influence of stochastic discrete jumps.
---
paper_title: A numerical approximation scheme for reachability analysis of stochastic hybrid systems with state-dependent switchings

paper_content:

We describe a methodology for reachability analysis of a certain class of stochastic hybrid systems, whose continuous dynamics is governed by stochastic differential equations and discrete dynamics by state-dependent probabilistic transitions. The main feature of the proposed methodology is that it rests on the weak approximation of the solution to the stochastic differential equation with random mode transitions by a Markov chain. Reachability computations then reduce to propagating the transition probabilities of the approximating Markov chain. An example of applications to system verification is presented.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---
paper_title: Approximation Metrics for Discrete and Continuous Systems

paper_content:

Established system relationships for discrete systems, such as language inclusion, simulation, and bisimulation, require system observations to be identical. When interacting with the physical world, modeled by continuous or hybrid systems, exact relationships are restrictive and not robust. In this paper, we develop the first framework of system approximation that applies to both discrete and continuous systems by developing notions of approximate language inclusion, approximate simulation, and approximate bisimulation relations. We define a hierarchy of approximation pseudo-metrics between two systems that quantify the quality of the approximation, and capture the established exact relationships as zero sections. Our approximation framework is compositional for a synchronous composition operator. Algorithms are developed for computing the proposed pseudo-metrics, both exactly and approximately. The exact algorithms require the generalization of the fixed point algorithms for computing simulation and bisimulation relations, or dually, the solution of a static game whose cost is the so-called branching distance between the systems. Approximations for the pseudo-metrics can be obtained by considering Lyapunov-like functions called simulation and bisimulation functions. We illustrate our approximation framework in reducing the complexity of safety verification problems for both deterministic and nondeterministic continuous systems
---
paper_title: Approximation and Weak Convergence Methods for Random Processes with Applications to Stochastic Systems Theory

paper_content:

Control and communications engineers, physicists, and probability theorists, among others, will find this book unique. It contains a detailed development of approximation and limit theorems and methods for random processes and applies them to numerous problems of practical importance. In particular, it develops usable and broad conditions and techniques for showing that a sequence of processes converges to a Markov diffusion or jump process. This is useful when the natural physical model is quite complex, in which case a simpler approximation la diffusion process, for example) is usually made.The book simplifies and extends some important older methods and develops some powerful new ones applicable to a wide variety of limit and approximation problems. The theory of weak convergence of probability measures is introduced along with general and usable methods (for example, perturbed test function, martingale, and direct averaging) for proving tightness and weak convergence.Kushner's study begins with a systematic development of the method. It then treats dynamical system models that have state-dependent noise or nonsmooth dynamics. Perturbed Liapunov function methods are developed for stability studies of nonMarkovian problems and for the study of asymptotic distributions of non-Markovian systems. Three chapters are devoted to applications in control and communication theory (for example, phase-locked loops and adoptive filters). Smallnoise problems and an introduction to the theory of large deviations and applications conclude the book.Harold J. Kushner is Professor of Applied Mathematics and Engineering at Brown University and is one of the leading researchers in the area of stochastic processes concerned with analysis and synthesis in control and communications theory. This book is the sixth in The MIT Press Series in Signal Processing, Optimization, and Control, edited by Alan S. Willsky.
---
paper_title: On the Approximation Quality of Markov State Models

paper_content:

We consider a continuous-time Markov process on a large continuous or discrete state space. The process is assumed to have strong enough ergodicity properties and to exhibit a number of metastable sets. Markov state models (MSMs) are designed to represent the effective dynamics of such a process by a Markov chain that jumps between the metastable sets with the transition rates of the original process. MSMs have been used for a number of applications, including molecular dynamics, for more than a decade. Their approximation quality, however, has not yet been fully understood. In particular, it would be desirable to have a sharp error bound for the difference in propagation of probability densities between the MSM and the original process on long timescales. Here, we provide such a bound for a rather general class of Markov processes ranging from diffusions in energy landscapes to Markov jump processes on large discrete spaces. Furthermore, we discuss how this result provides formal support or shows the limitations of algorithmic strategies that have been found to be useful for the construction of MSMs. Our findings are illustrated by numerical experiments.
---
paper_title: Optimal Control of Stochastic Hybrid Systems Based on Locally Consistent Markov Decision Processes

paper_content:

This paper applies a known approach for approximating controlled stochastic diffusion to hybrid systems. Stochastic hybrid systems are approximated by locally consistent Markov decision processes that preserve local mean and covariance. A randomized switching policy is introduced for approximating the dynamics on the switching boundaries. The validity of the approximation is shown by solving the optimal control problem of minimizing a cost until a target set is reached using dynamic programming. It is shown that using the randomized switching policy, the solution obtained based on the discrete approximation converges to the solution of the original problem
---
paper_title: Approximate Model Checking of Stochastic Hybrid Systems

paper_content:

A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system.
---
paper_title: Approximating stochastic biochemical processes with Wasserstein pseudometrics.

paper_content:

Modelling stochastic processes inside the cell is difficult due to the size and complexity of the processes being investigated. As a result, new approaches are needed to address the problems of model reduction, parameter estimation, model comparison and model invalidation. Here, the authors propose addressing these problems by using Wasserstein pseudometrics to quantify the differences between processes. The method the authors propose is applicable to any bounded continuous-time stochastic process and pseudometrics between processes are defined only in terms of the available outputs. Algorithms for approximating Wasserstein pseudometrics are developed from experimental or simulation data and demonstrate how to optimise parameter values to minimise the pseudometrics. The approach is illustrated with studies of a stochastic toggle switch and of stochastic gene expression in E. coli.
---
paper_title: Markov Models and Optimization

paper_content:

Analysis, probability and stochastic processes piecewise deterministic processes expectations and distributions control theory control by intervention.
---
paper_title: Markov Chains and Stochastic Stability

paper_content:

Meyn & Tweedie is back! The bible on Markov chains in general state spaces has been brought up to date to reflect developments in the field since 1996 - many of them sparked by publication of the first edition. The pursuit of more efficient simulation algorithms for complex Markovian models, or algorithms for computation of optimal policies for controlled Markov models, has opened new directions for research on Markov chains. As a result, new applications have emerged across a wide range of topics including optimisation, statistics, and economics. New commentary and an epilogue by Sean Meyn summarise recent developments and references have been fully updated. This second edition reflects the same discipline and style that marked out the original and helped it to become a classic: proofs are rigorous and concise, the range of applications is broad and knowledgeable, and key ideas are accessible to practitioners with limited mathematical background.
---
paper_title: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

paper_content:

In this work, probabilistic reachability over a finite horizon is investigated for a class of discrete time stochastic hybrid systems with control inputs. A suitable embedding of the reachability problem in a stochastic control framework reveals that it is amenable to two complementary interpretations, leading to dual algorithms for reachability computations. In particular, the set of initial conditions providing a certain probabilistic guarantee that the system will keep evolving within a desired 'safe' region of the state space is characterized in terms of a value function, and 'maximally safe' Markov policies are determined via dynamic programming. These results are of interest not only for safety analysis and design, but also for solving those regulation and stabilization problems that can be reinterpreted as safety problems. The temperature regulation problem presented in the paper as a case study is one such case.
---
paper_title: Bisimulation for Labelled Markov Processes

paper_content:

In this paper we introduce a new class of labelled transition systems - Labelled Markov Processes - and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou denition for discrete systems, is indeed an equivalence relation. This turns out to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Bisimulation for Labelled Markov Processes

paper_content:

In this paper we introduce a new class of labelled transition systems - Labelled Markov Processes - and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou denition for discrete systems, is indeed an equivalence relation. This turns out to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Weak Bisimulation for Fully Probabilistic Processes

paper_content:

Bisimulations that abstract from internal computation have proven to be useful for verification of compositionally defined transition systems. In the literature of probabilistic extensions of such transition systems, similar bisimulations are rare. In this paper, we introduce weak and branching bisimulation for fully probabilistic systems, transition systems where nondeterministic branching is replaced by probabilistic branching. In contrast to the nondeterministic case, both relations coincide. We give an algorithm to decide weak (and branching) bisimulation with a time complexity cubic in the number of states of the fully probabilistic system. This meets the worst case complexity for deciding branching bisimulation in the nondeterministic case. In addition, the relation is shown to be a congruence with respect to the operators of PLSCCS, a lazy synchronous probabilistic variant of CCS. We illustrate that due to these properties, weak bisimulation provides all the crucial ingredients for mechanised compositional veri�cation of probabilistic transition systems.
---
paper_title: Bisimulation for probabilistic transition systems: a coalgebraic approach

paper_content:

Abstract The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendler in terms of a set functor, which associates to a set its collection of simple probability distributions. This coalgebraic formulation makes it possible to generalize the concepts of discrete probabilistic transition system and probabilistic bisimulation to a continuous setting involving Borel probability measures. A functor ℳ 1 is introduced that yields for a metric space its collection of Borel probability measures. Under reasonable conditions, this functor exactly captures generalized probabilistic bisimilarity. Application of the final coalgebra paradigm to a functor based on ℳ 1 then yields an internally fully abstract semantical domain with respect to probabilistic bisimulation, which is therefore well suited for the interpretation of probabilistic specification and stochastic programming concepts.
---
paper_title: Bisimulation for Labelled Markov Processes

paper_content:

In this paper we introduce a new class of labelled transition systems - Labelled Markov Processes - and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete, it could be the reals, for example. We assume that it is a Polish space (the underlying topological space for a complete separable metric space). The mathematical theory of such systems is completely new from the point of view of the extant literature on probabilistic process algebra; of course, it uses classical ideas from measure theory and Markov process theory. The notion of bisimulation builds on the ideas of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result that we prove is that a notion of bisimulation for Markov processes on Polish spaces, which extends the Larsen-Skou denition for discrete systems, is indeed an equivalence relation. This turns out to be a rather hard mathematical result which, as far as we know, embodies a new result in pure probability theory. This work heavily uses continuous mathematics which is becoming an important part of work on hybrid systems.
---
paper_title: Approximate Model Checking of Stochastic Hybrid Systems

paper_content:

A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system.
---
paper_title: Correctness Issues of Symbolic Bisimulation Computation for Markov Chains ⋆

paper_content:

Bisimulation reduction is a classical means to fight the infamous state space explosion problem, which limits the applicability of automated methods for verification like model checking. A signature-based method, originally developed by Blom and Orzan for labeled transition systems and adapted for Markov chains by Derisavi, has proved to be very efficient. It is possible to implement it symbolically using binary decision diagrams such that it is able to handle very large state spaces efficiently. We will show, however, that for Markov chains this algorithm suffers from numerical instabilities, which often result in too large quotient systems. We will present and experimentally evaluate two different approaches to avoid these problems: first the usage of rational arithmetic, and second an approach not only to represent the system structure but also the transition rates symbolically. In addition, this allows us to modify their actual values after the quotient computation.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

paper_content:

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experiments or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of epsi-simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines epsi-(bi)simulation. Of course, for all the notions defined, letting epsi = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens in fully probabilistic systems when epsi = 0, two-way e-simulation for epsi > 0 is not equal to epsi-bisimulation. Next we give a polynomial time algorithm to compute a naturally derived metric: distance between states s and t is defined as the smallest epsi such that s and t are epsi-equivalent. This is the first polynomial algorithm for a non-discounted metric. Finally we show that most of these notions can be extended to deal with probabilistic systems that allow non-determinism as well.
---
paper_title: Approximate abstractions of stochastic systems: A randomized method

paper_content:

This work introduces a randomized method for the design of an approximate abstraction of a stochastic system and the assessment of its quality. The proposed approach relies on the formulation of the problem as a semi-infinite chance-constrained optimization program and on its solution via randomization. The method has quite general applicability, since it only requires to be able to run multiple executions of the candidate abstract model and of the original system and to compute their distance. Two variants of the notion of distance are considered in view of a possible use of the approximate abstraction for probabilistic safety verification. The approach is tested on a numerical example.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

paper_content:

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experiments or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of epsi-simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines epsi-(bi)simulation. Of course, for all the notions defined, letting epsi = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens in fully probabilistic systems when epsi = 0, two-way e-simulation for epsi > 0 is not equal to epsi-bisimulation. Next we give a polynomial time algorithm to compute a naturally derived metric: distance between states s and t is defined as the smallest epsi such that s and t are epsi-equivalent. This is the first polynomial algorithm for a non-discounted metric. Finally we show that most of these notions can be extended to deal with probabilistic systems that allow non-determinism as well.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

paper_content:

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experiments or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of epsi-simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines epsi-(bi)simulation. Of course, for all the notions defined, letting epsi = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens in fully probabilistic systems when epsi = 0, two-way e-simulation for epsi > 0 is not equal to epsi-bisimulation. Next we give a polynomial time algorithm to compute a naturally derived metric: distance between states s and t is defined as the smallest epsi such that s and t are epsi-equivalent. This is the first polynomial algorithm for a non-discounted metric. Finally we show that most of these notions can be extended to deal with probabilistic systems that allow non-determinism as well.
---
paper_title: Principles of Model Checking

paper_content:

Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.
---
paper_title: Labeled Markov processes: stronger and faster approximations

paper_content:

This paper proposes a measure-theoretic reconstruction of the approximation schemes developed for labeled Markov processes: approximants are seen as quotients with respect to sets of temporal properties expressed in a simple logic. This gives the possibility of customizing approximants with respect to properties of interest and is thus an important step towards using automated techniques intended for finite state systems, e.g. model checking, for continuous state systems. The measure-theoretic apparatus meshes well with an enriched logic, extended with a greatest fix-point, and gives means to define approximants which retain cyclic properties of their target.
---
paper_title: Approximate Abstractions of Stochastic Hybrid Systems

paper_content:

We present a constructive procedure for obtaining a finite approximate abstraction of a discrete-time stochastic hybrid system. The procedure consists of a partition of the state space of the system and depends on a controllable parameter. Given proper continuity assumptions on the model, the approximation errors introduced by the abstraction procedure are explicitly computed and it is shown that they can be tuned through the parameter of the partition. The abstraction is interpreted as a Markov set-Chain. We show that the enforcement of certain ergodic properties on the stochastic hybrid model implies the existence of a finite abstraction with finite error in time over the concrete model, and allows introducing a finite-time algorithm that computes the abstraction.
---
paper_title: Metrics for Markov Decision Processes with Infinite State Spaces

paper_content:

We present metrics for measuring state similarity in Markov decision processes (MDPs) with infinitely many states, including MDPs with continuous state spaces. Such metrics provide a stable quantitative analogue of the notion of bisimulation for MDPs, and are suitable for use in MDP approximation. We show that the optimal value function associated with a discounted infinite horizon planning task varies continuously with respect to our metric distances.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---
paper_title: Metrics for Labelled Markov Processes

paper_content:

The notion of process equivalence of probabilistic processes is sensitive to the exact probabilities of transitions. Thus, a slight change in the transition probabilities will result in two equivalent processes being deemed no longer equivalent. This instability is due to the quantitative nature of probabilistic processes. In a situation where the process behavior has a quantitative aspect there should be a more robust approach to process equivalence. This paper studies a metric between labelled Markov processes. This metric has the property that processes are at zero distance if and only if they are bisimilar. The metric is inspired by earlier work on logics for characterizing bisimulation and is related, in spirit, to the Hutchinson metric.
---
paper_title: Probabilistic bisimulations of switching and resetting diffusions

paper_content:

This contribution presents sufficient conditions for the existence of probabilistic bisimulations between two diffusion processes that are additionally endowed with switching and resetting behaviors. A probabilistic bisimulation between two stochastic processes is defined by means of a bisimulation function, which induces an approximation metric over the distance between the two processes. The validity of the proposed sufficient conditions results in the explicit characterization of one such bisimulation function. The conditions depend on contractivity properties of the two stochastic processes.
---
paper_title: Approximations of Stochastic Hybrid Systems

paper_content:

This paper develops a notion of approximation for a class of stochastic hybrid systems that includes, as special cases, both jump linear stochastic systems and linear stochastic hybrid automata. Our approximation framework is based on the recently developed notion of the so-called stochastic simulation functions. These Lyapunov-like functions can be used to rigorously quantify the distance or error between a system and its approximate abstraction. For the class of jump linear stochastic systems and linear stochastic hybrid automata, we show that the computation of stochastic simulation functions can be cast as a tractable linear matrix inequality problem. This enables us to compute the modeling error incurred by abstracting some of the continuous dynamics, or by neglecting the influence of stochastic noise, or even the influence of stochastic discrete jumps.
---
paper_title: Approximations of Stochastic Hybrid Systems

paper_content:

This paper develops a notion of approximation for a class of stochastic hybrid systems that includes, as special cases, both jump linear stochastic systems and linear stochastic hybrid automata. Our approximation framework is based on the recently developed notion of the so-called stochastic simulation functions. These Lyapunov-like functions can be used to rigorously quantify the distance or error between a system and its approximate abstraction. For the class of jump linear stochastic systems and linear stochastic hybrid automata, we show that the computation of stochastic simulation functions can be cast as a tractable linear matrix inequality problem. This enables us to compute the modeling error incurred by abstracting some of the continuous dynamics, or by neglecting the influence of stochastic noise, or even the influence of stochastic discrete jumps.
---
paper_title: Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games

paper_content:

We tackle the problem of non robustness of simulation and bisimulation when dealing with probabilistic processes. It is important to ignore tiny deviations in probabilities because these often come from experiments or estimations. A few approaches have been proposed to treat this issue, for example metrics to quantify the non bisimilarity (or closeness) of processes. Relaxing the definition of simulation and bisimulation is another avenue which we follow. We define a new semantics to a known simple logic for probabilistic processes and show that it characterises a notion of epsi-simulation. We also define two-players games that correspond to these notions: the existence of a winning strategy for one of the players determines epsi-(bi)simulation. Of course, for all the notions defined, letting epsi = 0 gives back the usual notions of logical equivalence, simulation and bisimulation. However, in contrast to what happens in fully probabilistic systems when epsi = 0, two-way e-simulation for epsi > 0 is not equal to epsi-bisimulation. Next we give a polynomial time algorithm to compute a naturally derived metric: distance between states s and t is defined as the smallest epsi such that s and t are epsi-equivalent. This is the first polynomial algorithm for a non-discounted metric. Finally we show that most of these notions can be extended to deal with probabilistic systems that allow non-determinism as well.
---
paper_title: Lyapunov-like techniques for stochastic stability

paper_content:

The purpose of this paper is to give a survey of the results proved in Florchinger (1993) concerning the stabilizability problem for control stochastic nonlinear systems driven by a Wiener process. Sufficient conditions for the existence of stabilizing feedback laws which are smooth, except possibly at the equilibrium point of the system, are provided by means of stochastic Lyapunov-like techniques. The notion of dynamic asymptotic stability in probability of control stochastic differential systems is introduced, and the stabilization by means of dynamic controllers is studied. >
---
paper_title: Approximately Bisimilar Symbolic Models for Incrementally Stable Switched Systems

paper_content:

Switched systems constitute an important modeling paradigm faithfully describing many engineering systems in which software interacts with the physical world. Despite considerable progress on stability and stabilization of switched systems, the constant evolution of technology demands that we make similar progress with respect to different, and perhaps more complex, objectives. This paper describes one particular approach to address these different objectives based on the construction of approximately equivalent (bisimilar) symbolic models for switched systems. The main contribution of this paper consists in showing that under standard assumptions ensuring incremental stability of a switched system (i.e., existence of a common Lyapunov function, or multiple Lyapunov functions with dwell time), it is possible to construct a finite symbolic model that is approximately bisimilar to the original switched system with a precision that can be chosen a priori. To support the computational merits of the proposed approach, we use symbolic models to synthesize controllers for two examples of switched systems, including the boost dc-dc converter.
---
paper_title: A contractivity approach for probabilistic bisimulations of diffusion processes

paper_content:

This work is concerned with the problem of characterizing and computing probabilistic bisimulations of diffusion processes. A probabilistic bisimulation relation between two such processes is defined through a bisimulation function, which induces an approximation metric on the expectation of the (squared norm of the) distance between the two processes. We introduce sufficient conditions for the existence of a bisimulation function, based on the use of contractivity analysis for probabilistic systems. Furthermore, we show that the notion of stochastic contractivity is related to a probabilistic version of the concept of incremental stability. This relationship leads to a procedure that constructs a discrete approximation of a diffusion process. The procedure is based on the discretization of space and time. Given a diffusion process, we raise sufficient conditions for the existence of such an approximation, and show that it is probabilistically bisimilar to the original process, up to a certain approximation precision.
---
paper_title: Approximately bisimilar symbolic models for nonlinear control systems

paper_content:

Control systems are usually modeled by differential equations describing how physical phenomena can be influenced by certain control parameters or inputs. Although these models are very powerful when dealing with physical phenomena, they are less suitable to describe software and hardware interfacing the physical world. For this reason there is a growing interest in describing control systems through symbolic models that are abstract descriptions of the continuous dynamics, where each "symbol" corresponds to an "aggregate" of states in the continuous model. Since these symbolic models are of the same nature of the models used in computer science to describe software and hardware, they provide a unified language to study problems of control in which software and hardware interact with the physical world. Furthermore the use of symbolic models enables one to leverage techniques from supervisory control and algorithms from game theory for controller synthesis purposes. In this paper we show that every incrementally globally asymptotically stable nonlinear control system is approximately equivalent (bisimilar) to a symbolic model. The approximation error is a design parameter in the construction of the symbolic model and can be rendered as small as desired. Furthermore if the state space of the control system is bounded the obtained symbolic model is finite. For digital control systems, and under the stronger assumption of incremental input-to-state stability, symbolic models can be constructed through a suitable quantization of the inputs.
---
paper_title: A Contraction Theory Approach to Stochastic Incremental Stability

paper_content:

We investigate the incremental stability properties of It\^o stochastic dynamical systems. Specifically, we derive a stochastic version of nonlinear contraction theory that provides a bound on the mean square distance between any two trajectories of a stochastically contracting system. This bound can be expressed as a function of the noise intensity and the contraction rate of the noise-free system. We illustrate these results in the contexts of stochastic nonlinear observers design and stochastic synchronization.
---
paper_title: Probabilistic bisimulations of switching and resetting diffusions

paper_content:

This contribution presents sufficient conditions for the existence of probabilistic bisimulations between two diffusion processes that are additionally endowed with switching and resetting behaviors. A probabilistic bisimulation between two stochastic processes is defined by means of a bisimulation function, which induces an approximation metric over the distance between the two processes. The validity of the proposed sufficient conditions results in the explicit characterization of one such bisimulation function. The conditions depend on contractivity properties of the two stochastic processes.
---
paper_title: Approximations of Stochastic Hybrid Systems

paper_content:

This paper develops a notion of approximation for a class of stochastic hybrid systems that includes, as special cases, both jump linear stochastic systems and linear stochastic hybrid automata. Our approximation framework is based on the recently developed notion of the so-called stochastic simulation functions. These Lyapunov-like functions can be used to rigorously quantify the distance or error between a system and its approximate abstraction. For the class of jump linear stochastic systems and linear stochastic hybrid automata, we show that the computation of stochastic simulation functions can be cast as a tractable linear matrix inequality problem. This enables us to compute the modeling error incurred by abstracting some of the continuous dynamics, or by neglecting the influence of stochastic noise, or even the influence of stochastic discrete jumps.
---
paper_title: Bisimilar linear systems

paper_content:

The notion of bisimulation in theoretical computer science is one of the main complexity reduction methods for the analysis and synthesis of labeled transition systems. Bisimulations are special quotients of the state space that preserve many important properties expressible in temporal logics, and, in particular, reachability. In this paper, the framework of bisimilar transition systems is applied to various transition systems that are generated by linear control systems. Given a discrete-time or continuous-time linear system, and a finite observation map, we characterize linear quotient maps that result in quotient transition systems that are bisimilar to the original system. Interestingly, the characterizations for discrete-time systems are more restrictive than for continuous-time systems, due to the existence of an atomic time step. We show that computing the coarsest bisimulation, which results in maximum complexity reduction, corresponds to computing the maximal controlled or reachability invariant subspace inside the kernel of the observations map. These results establish strong connections between complexity reduction concepts in control theory and computer science.
---
paper_title: Bisimilar control affine systems

paper_content:

The notion of bisimulation plays a very important role in theoretical computer science where it provides several notions of equivalence between models of computation. These equivalences are in turn used to simplify analysis and synthesis for these models. In system theory, a similar notion is also of interest in order to develop modular analysis and design tools for purely continuous or hybrid control systems. We introduce two notions of bisimulation for nonlinear systems. We present a differential-algebraic characterization of these notions and show that bisimilar systems of different dimensions are obtained by factoring out certain invariant distributions. Furthermore, we also show that all bisimilar systems of different dimension are of this form.
---
paper_title: Adaptive Gridding for Abstraction and Verification of Stochastic Hybrid Systems

paper_content:

This work is concerned with the generation of finite abstractions of general Stochastic Hybrid Systems, to be employed in the formal verification of probabilistic properties by means of model checkers. The contribution employs an abstraction procedure based on a partitioning of the state space, and puts forward a novel adaptive gridding algorithm that is expected to conform to the underlying dynamics of the model and thus at least to mitigate the curse of dimensionality related to the partitioning procedure. With focus on the study of probabilistic safety over a finite horizon, the proposed adaptive algorithm is first benchmarked against a uniform gridding approach from the literature, and finally tested on a known applicative case study.
---
paper_title: On Choosing and Bounding Probability Metrics

paper_content:

When studying convergence of measures, an important issue is the choice of probability metric. In this review, we provide a summary and some new results concerning bounds among ten important probability metrics/distances that are used by statisticians and probabilists. We focus on these metrics because they are either well-known, commonly used, or admit practical bounding techniques. We summarize these relationships in a handy reference diagram, and also give examples to show how rates of convergence can depend on the metric chosen.
---
paper_title: On infinite-horizon probabilistic properties and stochastic bisimulation functions

paper_content:

This work investigates infinite-horizon properties over discrete-time stochastic models with continuous state spaces. The focus is on understanding how the structural features of a model (e.g., the presence of absorbing sets) affect the values of these properties and relate to their uniqueness. Furthermore, we argue that the investigation of these features can lead to approximation bounds for the value of such properties, as well as to improvements on their computation. The article employs the presented results to find a stochastic bisimulation function of two processes.
---
paper_title: Approximate abstractions of stochastic systems: A randomized method

paper_content:

This work introduces a randomized method for the design of an approximate abstraction of a stochastic system and the assessment of its quality. The proposed approach relies on the formulation of the problem as a semi-infinite chance-constrained optimization program and on its solution via randomization. The method has quite general applicability, since it only requires to be able to run multiple executions of the candidate abstract model and of the original system and to compute their distance. Two variants of the notion of distance are considered in view of a possible use of the approximate abstraction for probabilistic safety verification. The approach is tested on a numerical example.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---
paper_title: A theory of timed automata

paper_content:

Alur, R. and D.L. Dill, A theory of timed automata, Theoretical Computer Science 126 (1994) 183-235. We propose timed (j&e) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Biichi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable (II i-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.
---
paper_title: Uncertain convex programs: Randomized solutions and confidence levels

paper_content:

Many engineering problems can be cast as optimization problems subject to convex constraints that are parameterized by an uncertainty or ‘instance’ parameter. Two main approaches are generally available to tackle constrained optimization problems in presence of uncertainty: robust optimization and chance-constrained optimization. Robust optimization is a deterministic paradigm where one seeks a solution which simultaneously satisfies all possible constraint instances. In chance-constrained optimization a probability distribution is instead assumed on the uncertain parameters, and the constraints are enforced up to a pre-specified level of probability. Unfortunately however, both approaches lead to computationally intractable problem formulations.
---
paper_title: Approximate Model Checking of Stochastic Hybrid Systems

paper_content:

A method for approximate model checking of stochastic hybrid systems with provable approximation guarantees is proposed. We focus on the probabilistic invariance problem for discrete time stochastic hybrid systems and propose a two-step scheme. The stochastic hybrid system is first approximated by a finite state Markov chain. The approximating chain is then model checked for probabilistic invariance. Under certain regularity conditions on the transition and reset kernels governing the dynamics of the stochastic hybrid system, the invariance probability computed using the approximating Markov chain is shown to converge to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided. The performance of the two-step approximate model checking procedure is assessed on a case study of a multi-room heating system.
---
paper_title: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

paper_content:

In this work, probabilistic reachability over a finite horizon is investigated for a class of discrete time stochastic hybrid systems with control inputs. A suitable embedding of the reachability problem in a stochastic control framework reveals that it is amenable to two complementary interpretations, leading to dual algorithms for reachability computations. In particular, the set of initial conditions providing a certain probabilistic guarantee that the system will keep evolving within a desired 'safe' region of the state space is characterized in terms of a value function, and 'maximally safe' Markov policies are determined via dynamic programming. These results are of interest not only for safety analysis and design, but also for solving those regulation and stabilization problems that can be reinterpreted as safety problems. The temperature regulation problem presented in the paper as a case study is one such case.
---
paper_title: The Scenario Approach for Systems and Control Design

paper_content:

The ‘scenario approach’ is an innovative technology that has been introduced to solve convex optimization problems with an infinite number of constraints, a class of problems which often occurs when dealing with uncertainty. This technology relies on random sampling of constraints, and provides a powerful means for solving a variety of design problems in systems and control. The objective of this paper is to illustrate the scenario approach at a tutorial level, focusing mainly on algorithmic aspects. Its versatility and virtues will be pointed out through a number of examples in model reduction, robust and optimal control.
---
paper_title: Approximating stochastic biochemical processes with Wasserstein pseudometrics.

paper_content:

Modelling stochastic processes inside the cell is difficult due to the size and complexity of the processes being investigated. As a result, new approaches are needed to address the problems of model reduction, parameter estimation, model comparison and model invalidation. Here, the authors propose addressing these problems by using Wasserstein pseudometrics to quantify the differences between processes. The method the authors propose is applicable to any bounded continuous-time stochastic process and pseudometrics between processes are defined only in terms of the available outputs. Algorithms for approximating Wasserstein pseudometrics are developed from experimental or simulation data and demonstrate how to optimise parameter values to minimise the pseudometrics. The approach is illustrated with studies of a stochastic toggle switch and of stochastic gene expression in E. coli.
---
paper_title: On Choosing and Bounding Probability Metrics

paper_content:

When studying convergence of measures, an important issue is the choice of probability metric. In this review, we provide a summary and some new results concerning bounds among ten important probability metrics/distances that are used by statisticians and probabilists. We focus on these metrics because they are either well-known, commonly used, or admit practical bounding techniques. We summarize these relationships in a handy reference diagram, and also give examples to show how rates of convergence can depend on the metric chosen.
---
paper_title: Labeled Markov processes: stronger and faster approximations

paper_content:

This paper proposes a measure-theoretic reconstruction of the approximation schemes developed for labeled Markov processes: approximants are seen as quotients with respect to sets of temporal properties expressed in a simple logic. This gives the possibility of customizing approximants with respect to properties of interest and is thus an important step towards using automated techniques intended for finite state systems, e.g. model checking, for continuous state systems. The measure-theoretic apparatus meshes well with an enriched logic, extended with a greatest fix-point, and gives means to define approximants which retain cyclic properties of their target.
---
paper_title: Approximating labeled Markov processes

paper_content:

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.
---

Title: Approximation Metrics Based on Probabilistic Bisimulations for General State-Space Markov Processes: A Survey

Section 1: Motivations and Objective
Description 1: Introduce the motivations for studying approximation metrics based on probabilistic bisimulations, and outline the objectives and structure of the survey.

Section 2: Review of Literature Background
Description 2: Provide a comprehensive coverage of existing work on simulations, bisimulations, and approximate versions thereof, specifically focusing on probabilistic models.

Section 3: Markov Processes over General State Spaces
Description 3: Introduce and discuss the models under study, particularly probabilistic processes defined over continuous state spaces.

Section 4: Exact and Approximate Probabilistic Bisimulations: Relations, Logics, and Categories
Description 4: Present the concept of exact and approximate (strong) probabilistic bisimulation, and provide related characterizations based on algebra, logic, and category theory.

Section 5: Approximate Bisimulations via Probabilistic Bisimulation Functions
Description 5: Define and characterize the notion of probabilistic bisimulation function, leading to the introduction of approximate metrics between processes' trajectories.

Section 6: Characterization of Stochastic Bisimulation Function as solution of a Probabilistic Reachability Problem
Description 6: Look at semantic-based computations of distance metrics between comparable probabilistic processes by solving probabilistic reachability problems.

Section 7: Discussion and Conclusions
Description 7: Discuss the surveyed techniques, highlight their differences, and look forward at future research directions and practical applications.