Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Backward and forward bisimulation minimization of tree automata

We improve on an existing [P.A. Abdulla, J. Högberg, L. Kaati, Bisimulation minimization of tree automata, International Journal of Foundations of Computer Science 18(4) (2007) 699–713] bisimulation minimization algorithm for finite-state tree automata by introducing backward and forward bisimulation and developing minimization algorithms for them. Minimization via forward bisimulation is also effective on deterministic tree automata, faster than the previous algorithm, and yields the minimal equivalent deterministic tree automaton. Minimization via backward bisimulation generalizes the previous algorithm and can yield smaller automata but is just as fast. We demonstrate implementations of these algorithms on a typical task in natural language processing.     

一种测试语言包含的算法

在积自动机基础上,利用互模拟关系引出商自动机,用以解决积自动机的状态组合爆炸问题。进而提出一个自然的测试语言包含的算法,这种算法的空间复杂度与规范自动机的状态目呈指数关系即O（2^k),其中K是规范自动机的状态数目。     

p-Automata: New foundations for discrete-time probabilistic verification

We introduce p-Automata, which are automata that accept languages of Markov chains, by adapting notions and techniques from alternating tree automata to the realm of Markov chains. The set of languages of p-automata is closed under Boolean operations, and for every PCTL formula it contains the language of the set of models of the formula. Furthermore, the language of every p-automaton is closed under probabilistic bisimulation. Similar to tree automata, whose acceptance is defined via two-player games, we define acceptance of Markov chains by p-automata through two-player stochastic games. We show that acceptance is solvable in EXPTIME; but for automata that arise from PCTL formulas acceptance matches that of PCTL model checking, namely, linear in the formula and polynomial in the Markov chain. We also derive a notion of simulation between p-automata that approximates language containment in EXPTIME and is complete for Markov chains. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics.     

A linear process-algebraic format with data for probabilistic automata

This paper presents a novel linear process-algebraic format for probabilistic automata. The key ingredient is a symbolic transformation of probabilistic process algebra terms that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalises similar techniques for traditional process algebras with data, and — more importantly — treats data and data-dependent probabilistic choice in a fully symbolic manner, leading to the symbolic analysis of parameterised probabilistic systems. We discuss several reduction techniques that can easily be applied to our models. A validation of our approach on two benchmark leader election protocols shows reductions of more than an order of magnitude.     

Bisimulation for Labelled Markov Processes

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. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems.

• Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.

• We do not need any finite branching assumption, yet there is no need of infinitary conjunction.

We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.     

Probabilistic Logical Characterization

Probabilistic automata exhibit both probabilistic and non-deterministic choice. They are therefore a powerful semantic foundation for modeling concurrent systems with random phenomena arising in many applications ranging from artificial intelligence, security, systems biology to performance modeling. Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. This paper develops a taxonomy of logical characterizations of these relations on image-finite and image-infinite probabilistic automata.     

On the minimization of XML Schemas and tree automata for unranked trees

Automata for unranked trees form a foundation for XML Schemas, querying and pattern languages. We study the problem of efficiently minimizing such automata. First, we study unranked tree automata that are standard in database theory, assuming bottom-up determinism and that horizontal recursion is represented by deterministic finite automata. We show that minimal automata in that class are not unique and that minimization is np-complete. Second, we study more recent automata classes that do allow for polynomial time minimization. Among those, we show that bottom-up deterministic stepwise tree automata yield the most succinct representations. Third, we investigate abstractions of XML schema languages. In particular, we show that the class of one-pass preorder typeable schemas allows for polynomial time minimization and unique minimal models.     

Relaxation labeling with learning automata

Relaxation labeling processes are a class of mechanisms that solve the problem of assigning labels to objects in a manner that is consistent with respect to some domain-specific constraints. We reformulate this using the model of a team of learning automata interacting with an environment or a high-level critic that gives noisy responses as to the consistency of a tentative labeling selected by the automata. This results in an iterative linear algorithm that is itself probabilistic. Using an explicit definition of consistency we give a complete analysis of this probabilistic relaxation process using weak convergence results for stochastic algorithms. Our model can accommodate a range of uncertainties in the compatibility functions. We prove a local convergence result and show that the point of convergence depends both on the initial labeling and the constraints. The algorithm is implementable in a highly parallel fashion.     

Multihead two-way probabilistic finite automata

We present properties of multihead two-way probabilistic finite automata that parallel those of their deterministic and nondeterministic counterparts. We define multihead probabilistic finite automata withlogspace constructible transition probabilities, and we describe a technique to simulate these automata by standard logspace probabilistic Turing machines. Next, we represent logspace probabilistic complexity classes as proper hierarchies based on corresponding multihead two-way probabilistic finite automata, and we show their (deterministic logspace) reducibility to the second levels of these hierarchies. We obtain a simple formula for the maximum inherent bandwidth of the configuration transition matrices associated with thek-head probabilistic finite automata processing a length-n input string. (The inherent bandwidth of the configuration transition matrices associated with an automaton processing a length-n input string is the smallest bandwidth we can get by changing the enumeration order of the automaton’s configurations.) Partially based on this relation, we find an apparently easier logspace complete problem forPL (the class of languages recognized by logspace unbounded-error probabilistic Turing machines), and we discuss possibilities for a space-efficient deterministic simulation of probabilistic automata.     

Greatest Bisimulations for Binary Methods

In previous work [14] I introduced a generalised notion of coalgebra that is capable of modelling binary methods as they occur in object-oriented programming. An important problem with this generalisation is that bisimulations are not closed under union and that a greatest bisimulation does not exists in general. There are two possible approaches to improve this situation: First, to strengthen the definition of bisimulation, and second, to place constraints on the coalgebras (i.e., on the behaviour of the binary methods). In this paper I combine both approaches to show that (under reasonable assumptions) the greatest bisimulation does exist for all coalgebras of extended polynomial functors.     

Checking Temporal Duration Properties of Timed Automata

In this paper, the problem of checking a timed automaton for a Duration Calculus formula of the form Temporal Duration Property is addressed. It is shown that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and an algorithm is given to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as that of the solution of the reachability problem of timed automata.     

Metrics for Action-labelled Quantitative Transition Systems

This paper defines action-labelled quantitative transition systems as a general framework for combining qualitative and quantitative analysis. We define state-metrics as a natural extension of bisimulation from non-quantitative systems to quantitative ones. We then prove that any single state-metric corresponds to a bisimulation and that the greatest state-metric corresponds to bisimilarity. Furthermore, we provide two extended examples which show that our results apply to both probabilistic and weighted automata as special cases of action-labelled quantitative transition systems.     

(r,t)阶存贮拟线性有限自动机的极小化

实现将一个有限自动机极小化是一个困难的问题。通过零状态考虑了一类(r,t)阶存贮拟线性有限自动机极小化的判断方法,给出了极小线性有限自动机的描述,最后给出了基于系数矩阵的极小化算法实现。     

A Probabilistic approach for model following of Markovian jump linear systems subject to actuator saturation

This paper is concerned with the model following problem of Markovian jump linear systems (MJLSs), which suffer from stochastic uncertainties and actuator saturation. By applying a probabilistic approach based on particles, a sequence of control inputs is designed to guarantee that the model following error remains within a desired region in a certain probability, as well as the control cost is optimal. Motivated by this, the stochastic control problem is represented by chance constrained programming, and approximated as a determinate optimization one, which is solved by mixed integer linear programming (MILP). Furthermore, an improved particle control approach is proposed to reduce the computation complexity. The effectiveness of this improved approach is demonstrated by an example along with complexity comparison.     

A logical duality for underspecified probabilistic systems

This paper establishes a Stone-type duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly, its simple structure can encode a mix of probabilistic and non-deterministic behavior, which, as we show, is strongly related to another well-known such model: probabilistic automata. Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories and show that we have an adjunct pair of functors when restricted to LMPs only. Our duality also shows that an infLMP can be considered as a demonic representative of a system’s information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics. This paper is an extended version of a Concur ’09 paper [13]; in particular, the comparison of infLMPs with probabilistic automata and the Galois connection are new.     

Average Case Analysis of Moore’s State Minimization Algorithm

We prove that the average complexity of Moore’s state minimization algorithm is $\mathcal {O}(kn\log n)$ , where n is the number of states of the input and k the size of the alphabet. This result holds for a whole family of probabilistic models on automata, including the uniform distribution over deterministic and accessible automata, as well as uniform distributions over classical subclasses, such as complete automata, acyclic automata, automata where each state is final with probability γ∈(0,1), and many other variations.     

Alternation on cellular automata

In this paper we consider several notions of alternation in cellular automata: non-uniform, uniform and weak alternation. We study relations among these notions and with alternating Turing machines. It is proved that the languages accepted in polynomial time by alternating Turing machines are those accepted by alternating cellular automata in polynomial time for all the proposed alternating cellular automata. In particular, this is true for the weak model where the difference between existential and universal states is omitted for all the cells except the first one. It is proved that real time alternation in cellular automata is strictly more powerful than real time alternation in Turing machines, with only one read-write tape. Moreover, it is shown that in linear time uniform and weak models agree.     

Bisimulation Minimization and Symbolic Model Checking

State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.     

Multihead Two-Way Probabilistic Finite Automata

We present properties of multihead two-way probabilistic finite automata that parallel those of their deterministic and nondeterministic counterparts. We define multihead probabilistic finite automata withlogspace constructible transition probabilities, and we describe a technique to simulate these automata by standard logspace probabilistic Turing machines. Next, we represent logspace probabilistic complexity classes as proper hierarchies based on corresponding multihead two-way probabilistic finite automata, and we show their (deterministic logspace) reducibility to the second levels of these hierarchies. We obtain a simple formula for the maximum inherent bandwidth of the configuration transition matrices associated with thek-head probabilistic finite automata processing a length-n input string. (The inherent bandwidth of the configuration transition matrices associated with an automaton processing a length-n input string is the smallest bandwidth we can get by changing the enumeration order of the automaton’s configurations.) Partially based on this relation, we find an apparently easier logspace complete problem forPL (the class of languages recognized by logspace unbounded-error probabilistic Turing machines), and we discuss possibilities for a space-efficient deterministic simulation of probabilistic automata. This research was supported by the National Science Foundation under Grant No. CDA 8822724 while the author was at the University of Rochester. An extended abstract of this paper appeared in Proceedings, Second Latin American Symposium, LATIN ’95: Theoretical Informatics, Valparaiso, Chile, April 1995.