Abstract Probabilistic Automata

Abstract Probabilistic Automata (Citations: 3)


	BibTex \| RIS \| RefWorks Download

, , , , , ,

Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behaviour is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.

Conference: Verification, Model Checking and Abstract Interpretation - VMCAI , pp. 324-339, 2011

DOI: 10.1007/978-3-642-18275-4_23

Cumulative Annual

View Publication

( www.springerlink.com )

( www.informatik.uni-trier.de )

- ...Due to space limitation, proofs and larger examples are given in a long version of this paper [10]...
- ...This operator is applied until a fixed point is reached, i.e., until the specification does not contain inconsistent states (it is locally consistent). See [10] for details...
- ...Proof. We present a sketch of the proof and refer to [10] for details...
- ...Finally, observe that the conjunction of two APAs with interval constraints is not necessarily an APA with interval constraints, but could be an APA whose constraints are systems of linear inequalities (see [10] for an example)...
- ...It is worth mentioning that any APA with a single valuation in the initial state can be turned into an APA in single valuation normal form that accepts the same set of implementations (see [10] for such a transformation that preserves determinism)...
- ...N]] . The reverse of the theorem also holds up to a syntactical transformation that preserves sets of implementations (see [10] for details)...
Benoît Delahaye, et al. Abstract Probabilistic Automata
- ...Recently[8], we have proposed Abstract Probabilistic Automata (APAs), that is a compact abstraction formalism for sets of PAs...
- ...One of the major contributions of [8] was to develop the first specification theory for PAs...
- ...� We show that the definition of conjunction proposed in [8] is too strong for non-deterministic APAs...
- ...We propose a more general construction that corresponds to the greatest lower bound with respect to a new refinement relation, more precise than refinements introduced before[8]...
- ...We now briefly introduce the specification theory of Abstract Probabilistic Automata as presented in [8]...
- ...We begin by relating distributions between sets of states [8]:...
- ...Now, the following definition, originating in [8], formally establishes the roles of PAs and APAs as implementations and specifications respectively...
- ...In [8], a pruning operator � is defined that filters out distributions leading to inconsistent states, making these states unreachable...
- ...For this reason [8] introduces a more syntactic refinement, called a weak refinement:...
- ...The weak refinement is sound with respect to the thorough refinement: if N � N 0 then JNK � JN 0 K [8]...
- ...that the two refinements coincide for deterministic APAs if the initial state admits exactly one labeling: (jV (s0) j= 1) [8]...
- ...To conclude this section, we present the definition of parallel composition, which is known to be a precongruence with respect to weak refinement [8]...
- ...In [8], conjunction was only defined for action-deterministic APAs with identical alphabets...
- ...Then we generalize it to the non-deterministic case with dissimilar alphabets. Let’s recall the definition given in [8]:...
- ...In [8] it is shown that this construction captures the greatest lower-bound with respect to weak refinement, i.e...
- ...5), along with the so called strong refinement [8], had been introduced for Constraint Markov Chains in [9], as syntax directed sound characterizations of thorough refinement...
- ...They were then generalized to APAs in [8] in a “natural” way...
- ...As we see from Lemma 1 the conjunction construction of [8] is too strong with respect to the weak refinement for nondeterministic systems...
- ...First, strengthening the refinement makes it even more strong with respect to thorough refinement (so it becomes less precise which is undesirable), and moreover the known strong refinement [8] still violates Lemma 1 (i.e...
- ...In [8] we show how every APA can be normalized without changing its semantics...
- ...Still, this trick cannot be used for strong refinement, as defined in [8]...
- ...In [8], we have introduced the first complete specification theory for PAs with a comparison operator and both logical and structural composition...
Benoît Delahaye, et al. New Results on Abstract Probabilistic Automata
- ...Recently [2], [3], we proposed Abstract Probabilistic Automata (APA), a new powerful abstraction formalism for PAs equipped with (1) a series of aggressive abstraction techniques for state-space reduction, and (2) a specification theory for component-based design in the spirit of [4]...
- ...μ(s3) else. For all distributions μ that satisfies ϕ, μδ will satisfy ϕ � , and for all pairs (s, s � ) such that δ(s)(s � ) > 0, s R s � . Details can be found in [2], [3]...
Benoît Delahaye, et al. APAC: A Tool for Reasoning about Abstract Probabilistic Automata