Albert Benveniste

Jean-Baptiste Raclet
email: jean-baptiste.raclet@irit.fr

Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism

Keywords: factor graphs, Bayesian networks, nondeterminism, probabilistic automata, probabilistic programming graphes factoriels, réseaux Bayésiens, nondéterminisme, automates probabilistes, programmation probabiliste

Graphical models in probability and statistics are a core concept in the area of probabilistic reasoning and probabilistic programming-graphical models include Bayesian networks and factor graphs. In this paper we develop a new model of mixed (nondeterministic/probabilistic) automata that subsumes both nondeterministic automata and graphical probabilistic models. Mixed Automata are equipped with parallel composition, simulation relation, and support message passing algorithms inherited from graphical probabilistic models. Segala's Probabilistic Automata can be mapped to Mixed Automata.

Introduction

Context

Bayesian graphical modeling and inference [START_REF] Dempster | A generalization of bayesian inference[END_REF] expanded since the 1980's, with applications in numerous areas. Graphical models were introduced in probability and statistics to allow for a modular description of models [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF]. Graphical models divide into two subfamilies: (directed) Bayesian Networks originally proposed by Judea Pearl [START_REF] Pearl | Fusion, propagation, and structuring in belief networks[END_REF] and (nondirected) Factor Graphs [START_REF] Kindermann | Markov random fields and their applications[END_REF][START_REF] Loeliger | An introduction to factor graphs[END_REF][START_REF] Van De Meent | An introduction to probabilistic programming[END_REF]. Probabilistic graphical modeling gave birth to an important sub-community of probabilistic programming [START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF][START_REF] Plummer | JAGS: A program for analysis of Bayesian graphical models using Gibbs sampling[END_REF][START_REF] Van De Meent | An introduction to probabilistic programming[END_REF].

Factor Graphs allow for the modular specification of unnormalized probabilities, based on a nondirected bipartite graph (V, F, E), where V ∪F is the set of vertices and E⊆V ×F is the set of edges; let V f be the subset of v∈V such that (v, f )∈E. V is a set of random variables, and, to each factor f ∈F is associated an unnormalized probability p f (V f ) for the tuple V f of random variables. This model defines the unnormalized probability distribution of V as the product P (V ) = f ∈F p f (V f )-logarithms of probabilities are often considered instead and added, under the name of potential [START_REF] Kindermann | Markov random fields and their applications[END_REF].

A Bayesian Network is a tuple (V, E, p), where: V is a set of random variables; (V, E) is an acyclic directed graph (for each v∈V , we let pa(v) denote its parents); p(v|pa(v)) specifies, for each valuation of the parents pa(v), a conditional distribution for the variable v. The semantics of a Bayesian Network is that the joint distribution of V factorizes as the product P (V ) = v∈V p(v|pa(v)). Bayesian Networks are thus causal graphical probabilistic models and the specification of causality comes extra to the specification of the underlying probability distribution, in the form of directed branches of the graph. As pointed out by Judea Pearl [START_REF] Pearl | Causality[END_REF], causality is an extra information relating random variables, not inferrable from their joint probability distribution. Message passing algorithms are a key tool for Factor Graphs, allowing to map a subclass of them to Bayesian networks, see [START_REF] Loeliger | An introduction to factor graphs[END_REF] and Section 3.6 of [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF]. Through the union of underlying graphs and the compositional nature of probabilities specified by graphical probabilistic models, both frameworks of Bayesian Networks and Factor Graphs are naturally equipped with some kind of parallel composition. All these features explain why graphical models are considered as an intermediate format targeted by some probabilistic programming tools, see, e.g., [START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF][START_REF] Plummer | JAGS: A program for analysis of Bayesian graphical models using Gibbs sampling[END_REF], and [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF], chapter 3.

One important issue is the combination of probabilistic and nondeterministic behaviors. In statistical decision procedures, deciding whether the distribution of an observed sample belongs to subset P 1 or P 2 of probability distributions (where these subsets have empty intersection), exhibits nondeterminism in that the actual distribution is freely chosen within one of the two alternatives; this blending of probabilistic and nondeterministic behaviors is addressed in this case by using generalized likelihood ratio (GLR) tests [START_REF] Lehmann | Testing statistical hypotheses[END_REF]. Also, the mixing of probabilistic behaviors and nondeterminism is central in probabilistic programming [START_REF] Mciver | Abstraction, Refinement and Proof for Probabilistic Systems[END_REF][START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF][START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF]. How to blend probabilistic and nondeterministic behaviors in general is, therefore, an important issue.

Probabilistic Programming [START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF][START_REF] Plummer | JAGS: A program for analysis of Bayesian graphical models using Gibbs sampling[END_REF][START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF][START_REF] Olmedo | Conditioning in probabilistic programming[END_REF][START_REF] Katoen | Understanding probabilistic programs[END_REF][START_REF] Van De Meent | An introduction to probabilistic programming[END_REF][START_REF] Baudart | Reactive probabilistic programming[END_REF] provides support for specifying statistical models with modularity and libraries for performing inference. Some probabilistic languages generate likelihood functions [START_REF] Plummer | JAGS: A program for analysis of Bayesian graphical models using Gibbs sampling[END_REF][START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF][START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF] for use by inference algorithms, whereas other generate sampling procedures [START_REF] Goodman | Church: a language for generative models[END_REF][START_REF] Noah | The Design and Implementation of Probabilistic Programming Languages[END_REF]. Recently, G. Baudart et al. [START_REF] Baudart | Reactive probabilistic programming[END_REF] proposed reactive probabilistic programming of dynamical systems as a conservative extension of synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF], by enhancing the Hybrid Systems modeling language Zelus [START_REF] Benveniste | Building a hybrid systems modeler on synchronous languages principles[END_REF] with probabilities. Objectives of Probabilistic Programming can be categorized as follows:

1. Modeling paradigm. Blending probability and nondeterminism, composing, comparing (equivalence), are the main issues.

Inria 2. Model for proof systems. Calculi and their decidability and complexity are central issues in this objective.

3. Support for statistical inference, decision, and learning. Key pillars are all limit theorems of probability and statistics (law of large numbers, central limit theorem, large deviations). These theorems rely on stationarity (or time invariance) of the underlying probabilistic model. For models with no dynamics, independent identically distributed (i.i.d.) sets of data can be sampled from the model. For models with dynamics (e.g., Markov chains), runs can be observed and used to infer model characteristics. One central difficulty in this objective is the blending of nondeterminism with probabilities, as it generally breaks the stationarity of the underlying statistical model. For example, if two different statistical models are combined with a nondeterministic choice (or an if-then-else statement with nondeterministic guard), then stationarity of the overall model no longer holds. The solution is to recover stationary models by separating the two alternatives and not mixing them. This quickly becomes cumbersome if several such constructions are used in a model. This difficult and central issue is extensively discussed in [START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF], where it is shown that some major probabilistic programming tools may not correctly implement Monte-Carlo based learning algorithms such as Metropolis-Hastings.

Contribution

To illustrate our purpose, we begin with a toy example. Throughout this paper, all variables possess finite or denumerable type-this restriction is motivated by technical reasons explained later. Hence, types will not be declared when presenting examples. In "if-then-else" statements, it is understood that the control variable is Boolean. Consider the following discrete time dynamical system (universal quantifier ∀n is implicit):

S 1 :        observe u x 0 = c x x n = ϕ(u n , x n-1 ) y n = if f n then ψ(x n , v n ) else x n (1)
Model (1) involves signals, i.e., sequences, indexed by the natural integer n, of variables having the same type: for instance, signal x n denotes the sequence {x k | k∈N}. In (1), f n is a boolean signal indicating the occurrence of a failure and v n is a noise, i.e., some kind of disturbance. When a failure occurs, signal x n gets corrupted by noise v n , which is captured by the (unspecified) function ψ; otherwise, y n = x n . Since model (1) involves the delayed signal x n-1 , an initial condition for this signal is specified by x 0 = c x , where c x is some constant of same type as signal x n . Model (1) looks like a dynamical system as usual, with inputs u, f , and v, state x, and output y.

We are interested in a different interpretation, however, by which model (1) specifies what is observed/unobserved: u n is observed at every instant (as stated in the first line), whereas other signals are unobserved (this is the default case). From this perspective, signals f, v, x, and y are unknown and otherwise subject to (1). Thus, model (1) involves nondeterminism.

Next, consider the following stochastic model for noise v n :

S 2 : v n ∼ µ (2)
where v n ∼ µ means that variable v n has distribution µ at each instant n. As an important convention of our modeling framework, statement v n ∼ µ, taken in isolation, also means that the random sequence v n is independent, identically distributed (i.i.d.). No signal is observed in this model (capturing that we are considering an unobserved disturbance).

Having the two models S 1 and S 2 , we like to compose them, thus considering S 1 S 2 , defined as the conjunction of the two systems of equations (1,[START_REF] Abbes | Synchronization of bernoulli sequences on shared letters[END_REF]. S 1 S 2 combines stochastic behavior with nondeterminism (since failure signal f n is still unknown and unobverved). As a consequence of this composition, the nature of signal y n may or may not involve randomness, due to the if-then-else statement occurring in S 1 .

Consider next the following S 3 model specifying the behavior of the failure signal f :

S 3 :    f 0 = F f n = (rf n or f n-1 )
and not bk n rf n ∼ Bernoulli(10 -6 )

In this model, "root failure" signal rf is modeled as a Bernoulli sequence, i.e., P (rf = T) = 10 -6 ; boolean signal bk indicates that a "backup sensor" is provided. Thus, a failure is raised (f = T) if a root failure occurs, and it remains subsequently raised, until a backup sensor is provided. In S 3 , no signal is observed, thus bk is nondeterministic. Model (3) is mixed probabilistic/nondeterministic. If bk was specified as being observed, this model would become probabilistic in that, once the value of random signal rf n is known, the actual value of f n is determined. The next step is to further compose S 1 S 2 with S 3 . By convention of the parallel composition, as a consequence of composing the two statements "v n ∼ µ" and "rf n ∼ Bernoulli (10 -6 )", the two random sequences v n and rf n are mutually independent.

As a safety issue, we could be interested in evaluating the risk of missing an alarm raised by having signal y exceeding some threshold: an alarm is raised when y n > y max . This alarm triggers some reconfiguration, not shown here. This reconfiguration action was designed to act under the hypothesis that the system is fault-free, i.e., y n = x n always holds. Consider the following question: what is the "risk" that an alarm is missed when it should have occured, due to a fault? More precisely, what is the risk that "x n > y max and y n ≤ y max " occurs? (4) So far we did not define what we mean by "risk". It cannot be measured by a probability, since S 1 S 2 S 3 mixes probability with nondeterminism. By "risk" we mean a pessemistic evaluation of this probability, with nondeterminism acting as an adversary. Suppose, next, that we want to specify that signal y is observed in system S 1 S 2 S 3 . To this end, we consider the system

S 4 : observe y (5)
where no dynamics is otherwise specified. Parallel composition S 1 S 2 S 3 S 4 expands as the following model:

           observe u, y x 0 = c x , v 0 = c v , f 0 = F x n = ϕ(u n , x n-1 ) y n = if f n then ψ(x n , v n ) else x n f n = (rf n or f n-1 ) and not bk n (6)    rf n ∼ Bernoulli(10 -6 ) v n ∼ µ (rf n and v n are mutually independent i.i.d. signals) (7)

Inria

The intended semantics of model (6,7) is as follows: [START_REF] Abbes | Concurrency, sigma-algebras, and probabilistic fairness[END_REF] specifies the prior distribution of the pair (v, rf ) of random signals, where, by convention, the two signals are considered independent. ( 6) defines a constraint on the tuple of variables involved in the system. The observe constraint on the pair u, y states that its joint trajectory is given (through the sensors). As a consequence, the pair (v, rf ) of random signals is now equipped with the posterior distribution resulting from constraint (6) being enforced.

If we regard systems S 1 , . . . , S 4 as boxes with wires (the involved signals), this modeling approach naturally leads to graphical models alike Factor Graphs. Indeed, this way of specifying mixed probabilistic/nondeterministic systems is fully modular: component models can be freely assembled to yield system models. Primitive statements are: 1) declarations of prior distributions; 2) declarations of constraints on signals through equations relating them, implicitly resulting in the definition of a posterior distribution; and 3) a parallel composition in which composing prior distributions considers them independent and systems of equations are composed as usual. Closest to this approach are [START_REF] Baudart | Reactive probabilistic programming[END_REF] (born from synchronous programming [START_REF] Benveniste | The synchronous languages 12 years later[END_REF]) or [START_REF] Gupta | Stochastic processes as concurrent constraint programs[END_REF] (born from concurrent constraint programming).

As a semantic domain for the above modeling approach, we propose a framework subsuming graphical probabilistic modeling and supporting both probabilistic and nondeterministic behaviors. We focus our effort on semantics issues, such as: What is actually the probabilistic model specified? Given seemingly different system specifications, are they equivalent or do they differ? Can one define a parallel composition of models? With reference to the context of probabilistic programming recalled in Section 1.1, our work focuses on objective 1 only, with no consideration of other objectives.

One of our contributions is the model of Mixed Automata. Its design relies on a very simple idea. An automaton is specified through its set of transitions q α -→ q , where q and q are the current and next state, and α is the action triggering the transition. Upgrading this model to Probabilistic Automata [START_REF] Lynch | Compositionality for probabilistic automata[END_REF] consists in upgrading transitions to q α -→ π , where π is the next probabilistic state (a probability distribution over the set Q of states), from which the next state is derived by probabilistic sampling π q . The final upgrade to Mixed Automata is by upgrading such transitions to q α -→ S , where S is now a Mixed System (or Mixed Probabilistic/Nondeterministic System in its extended name), from which the next state is derived by sampling S q . Initially proposed in [START_REF] Benveniste | A calculus of stochastic systems for the specification, simulation, and hidden state estimation of mixed stochastic/nonstochastic systems[END_REF], Mixed Systems are pairs consisting of a private probability space and a visible state space, related through a relation. This pair specifies a posterior distribution, namely the conditional distribution given that the relation between states and random outcomes is satisfied. Visible states are exposed for possible interaction with other Mixed Systems. This allows to equip Mixed Systems with a parallel composition, on top of which a parallel composition for Mixed Automata can be defined. We show that Mixed Systems naturally inherit a notion of graphical structure, which subsumes both Bayesian Networks and Factor Graphs. Mixed Systems offer the counterpart of angelic/demonic nondeterminism [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF] and hard/soft conditioning [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF][START_REF] Tolpin | Probabilistic programs with stochastic conditioning[END_REF], which are important notions in probabilistic programming.

Mixed Automata, defined on top of Mixed Systems, naturally inherit their associated graphical structure and parallel composition. Mixed Automata are equipped with all the fundamental modular notions for Automata, namely the notions of (bi)simulation relation and parallel composition. In this paper, we show in addition that Mixed Automata subsume, in part, Segala's Probabilistic Automata (PA) [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF] and their variants. More precisely, we exhibit mappings from different PA models to Mixed Automata, preserving simulation equivalence. The parallel compositions, however, are most of the time different-we claim ours to be more useful than PA parallel composition when the two differ. In addition, in contrast to PA, our model of Mixed Au-tomata naturally captures the notion of posterior (conditional) distribution and offers a notion of graphical model.

The paper is organized as follows. Mixed Systems are introduced and further studied in Section 2. Mixed Automata are introduced and studied in Section 3, and then compared to Probabilistic Automata in Section 4. Related work is discussed more broadly in Section 5. Missing proofs are deferred to appendices. Focused bibliographical discussions are presented following each important notion. The reason is that the same mathematical notion occurs in different communities, under different names; so we felt it useful to relate them. Finally, Appendix D presents hints for extending our approach to continuous probability distributions.

2 Mixed Probabilistic/Nondeterministic Systems X shall denote an underlying set of variables, of finite domain. Elements of X are denoted by lower case letters x, y, z . . . , and finite subsets of X are denoted by upper case letters X, Y, Z. We use set theoretic operations on sets of variables. Whenever convenient, we regard X, Y, Z as tuples. The domain of x is denoted by Q x and the domain of

X is Q X = def x∈X Q x ,
we call it the state space; the generic element of Q X is called a state and is denoted by q X or simply q.

The pair (Ω, π) shall denote a discrete probability space, i.e., π is a countably additive function, from 2 Ω to [0, 1], such that π(∅) = 0 and π(Ω) = 1. We simply write π(ω) instead of π({ω}). The support of π is the set supp

(π) = def {ω | π(ω) > 0}. For a subset W ⊆Ω such that π(W )>0, the conditional probability π(V |W ) = def π(V ∩W ) π(W ) is well defined.
Finally, we will consider relations (or constraints) C ⊆ Ω × Q. Relations are composed by intersection.

Disclaimer: in this paper, we consider only discrete probability spaces: This restriction is technically important, since it allows for a straightforward definition of conditional probabilities, and the notion of support of a probability is easily defined. For the general case, the notion of conditional expectation is always defined [START_REF] Dellacherie | Probabilities and potentials[END_REF], whereas conditional distributions require additional topological assumptions for their existence, and so does the notion of support. To keep our work simpler, we decided not to cover those extensions. Appendix D presents hints for extending our approach to continuous probability distributions.

Mixed Systems, parallel composition, and Factor Graphs

In this section we introduce Mixed Systems and show that they extend and subsume in a unified framework: nondeterminism, probability spaces, and factor graphs. This section is inspired in part by [START_REF] Benveniste | A calculus of stochastic systems for the specification, simulation, and hidden state estimation of mixed stochastic/nonstochastic systems[END_REF]. The intuition is illustrated on Figure 1, which will guide us for the different notions attached to Mixed Systems. A Mixed System will be a pair, consisting of a probability space (Ω, π) and a Inria state space Q collecting the configurations of a tuple of state variables (here: x and y), related by a relation C. The probability space is "private", in that it is not directly exposed to any interaction with the environment. Interactions with the environment only occur through the state variables, thus seen as "visible". This distinction private/visible is shown on Figure 1 by the outgoing pins x, y, which contrast with the absence of outgoing pin for the probabilistic box.

x y Q C (Ω, π)
We are interested in understanding how Mixed Systems are "executed" (we call this the sampling), and how state properties-which are not by themselves random-can still get some kind of probabilistic evaluation.

Definition 1 (Mixed System, definition and semantics)

1. A Mixed System (or system for short) is a tuple S = (Ω, π, X, C), where: (Ω, π) is a probability space; X is a finite set of variables with domain Q = x∈X Q x ; and C ⊆ Ω×Q is a relation. In the sequel, we write ωCq to mean (ω, q)∈C.

2. S is called consistent if π(Ω c ) > 0,
where Ω c = def {ω∈Ω | ∃q : ωCq}. If S is consistent, its sampling is well defined and consists in:

(a) sampling ω∈Ω according to conditional probability π c , where:

∀A ⊆ Ω : π c (A) = def π(A | Ω c ) = π(A∩Ω c ) π(Ω c ) , (8)
(b) and, then, nondeterministically selecting q∈Q such that ωCq.

This two-step procedure is denoted by S q.

3. If S is consistent, its probabilistic semantics is defined as the pair π, π : 2 Q → [0, 1], where, for any state property A ⊆ Q:

π(A) = def π c (Ω ∃A )
where

Ω ∃A = def {ω ∈ Ω | ∃q ∈ A : ωCq} , (9)
π(A) = def π c (Ω ∀A )
where

Ω ∀A = def {ω ∈ Ω | ∀q ∈ A : ωCq} , (10)
The following generalized likelihood : 2 Q → [0, 1] is also of interest:

(A) = def max ω∈Ω ∃A π c (ω) . (11)
In the sequel, we shall denote by S(X) the class of all (possibly inconsistent) Mixed Systems having X as their set of variables.

π defined by formula ( 9) is not a probability on Q, but only an outer probability 1 , i.e., a function

π : 2 Q → [0, 1] such that π(∅) = 0, π(Q) = 1
, and π is sub-additive, meaning that it satisfies

∀A, (A n ) n∈N subsets of Q : A ⊆ n∈N A n =⇒ π(A) ≤ n∈N π(A n ) .
Note that (11) resembles (9) if we rewrite the latter as π(A) = ω∈Ω ∃A π c (ω). The same comments hold, mutatis mutandis, regarding the inner probability π, which is super-additive. Note that, if A = {q} is a singleton, then π(A) = π(A).

(

) 12
1 sometimes called also exterior or upper probability.

RR n°9447

Example 1 [Specializing to pure nondeterministic systems] A pure nondeterministic system is specified as a subset C ⊆ Q of the state space. To reformulate it as a Mixed System, simply take (Ω, π) trivial, i.e., Ω = {ω}, a singleton, equipped with the trivial probability such that π(ω) = 1, and define ωCq iff q ∈ C.

Example 2 [Specializing to pure probabilistic systems] A pure probabilistic system is specified as a pair (Ω, π). To reformulate as a Mixed System, take Q = Ω, and let C be the diagonal of Ω × Q; finally, let x be the variable with domain Q.

Discussion 1 (blending nondeterminism and probability) To capture the blending of nondeterminism and probability, outer probabilities are directly used in the Dempster-Shafer theory of evidence [START_REF] Dempster | Upper and lower probabilities induced by a multivalued mapping[END_REF][START_REF] Dempster | A generalization of bayesian inference[END_REF][START_REF] Shafer | A Mathematical Theory of Evidence[END_REF]]. 2 Outer probabilities do not support key limit theorems for use in statistics, such as the law of large numbers, the central limit theorem, and more. Hence, whereas the theory of evidence comes with reasoning capabilities, it does not directly support learning or estimation.

In formal methods for probabilistic systems (in the context of imperative programming), the blending of probability and nondeterminism was addressed by a number of authors, see, e.g., [START_REF] Den Hartog | Verifying probabilistic programs using a hoare like logic[END_REF][START_REF] Mciver | Abstraction, Refinement and Proof for Probabilistic Systems[END_REF][START_REF] Barthe | Relational reasoning via probabilistic coupling[END_REF][START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF][START_REF] Katoen | Understanding probabilistic programs[END_REF][START_REF] Olmedo | Conditioning in probabilistic programming[END_REF][START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF][START_REF] Wang | A denotational semantics for low-level probabilistic programs with nondeterminism[END_REF]. Nondeterministic choice between alternatives is considered in [START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF] and written P P , whereas probabilistic choice is specified as P a ⊕ P (P is selected with probability a and P with probability 1-a) or P a ⊕ b P (P is selected with probability at least a and P with probability at least b). The evaluation of formulas must specify how nondeterminism interplays with probabilities. A comprehensive approach was proposed in [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF], where demonic and angelic nondeterminisms are seen as adversarial and beneficial, respectively. These notions mirror the outer and inner probabilities used in Dempster theory. Unfortunately, outer and inner probabilities do not bring limit theorems of probability theory (law of large numbers, etc.), which are the core of machine learning.

Through formulas [START_REF] Baudart | Reactive probabilistic programming[END_REF][START_REF] Bellman | A markovian decision process[END_REF] in Definition 1, the probabilistic semantics of Mixed Systems is defined as the associated outer and inner probabilities. Hence, Mixed Systems offer the calculus of the theory of evidence, and mirror the demonic and angelic types of nondeterminism. On the other hand, since classical probability spaces are first class citizens of the model of Mixed Systems, this model also preserves the apparatus needed for machine learning. In Appendix A.1, we develop a more detailed comparison of the semantics of Mixed Systems versus imperative probabilistic programming with demonic and angelic nondeterminism, following [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF].

Finally, the generalized likelihood of formula [START_REF] Benveniste | Building a hybrid systems modeler on synchronous languages principles[END_REF] is the basis for inference, estimation, or machine learning, when multiple hypotheses or nuisance parameters are considered [START_REF] Lehmann | Testing statistical hypotheses[END_REF]-we are not aware of any use of a mirror notion where "min" would be substituted for "max".

Example 3 [outer probabilities] Consider model S 1 S 2 S 3 of Section 1.2. Pick an instant n and let S = def S(n, x n-1 , f n-1 ) be the Mixed System defined by (1,2,3) for instant n and given values for x n-1 , f n-1 . With reference to (4), we wish to evaluate the probability that x n > y max and y n ≤ y max occurs under adversarial nondeterminism. Denoting by Q v the domain of v and by B the Boolean domain, the underlying probability space of S is (Ω, π), where Ω = Q v ×B and π = µ×β, where β is Bernoulli (10 -6 ). Domain Q for the variables of S is Q = Q x ×Q y ×Q u ×Q v ×B×B, and relation C is defined by the nonprobabilistic equations of S, i.e., (1,[START_REF] Abbes | Markovian dynamics of concurrent systems[END_REF] in which we discard the statement rf n ∼ β. Finally, let C(u n ) denote the relation C in which the value of u n is given (u is observed). Then π(x n >y max and y n ≤y max ) = π c (W ) , where W = (v, rf ) ∃x n , y n , f n , bk n :

x n >y max and y n ≤y max , and

(x n , y n , f n , bk n , v, rf ) ∈ C(u n ) (13)
Inspecting (1,[START_REF] Abbes | Markovian dynamics of concurrent systems[END_REF] shows that the condition defining set W rewrites as

x n >y max and ψ(x n , v)≤y max and f n =T and

(x n , y n , f n , bk n , v, rf ) ∈ C(u n ) .
First, if ϕ(u n , x n-1 ) ≤ y max holds, then W = ∅. We thus assume in the sequel ϕ(u n , x n-1 ) > y max . Thus we need to evaluate with respect to π the predicate

Z = def ψ(x n , v)≤y max and f n =T and (x n , y n , f n , bk n , v, rf ) ∈ C(u n ) .
Condition f n =T is equivalent to the conjunction of the following two conditions: 1) bk n =F (backup sensor is not available), 2) f n-1 =T or rf n =T. Recall that the value of f n-1 is given. We thus distinguish the following two cases:

1. f n-1 =T: then, f n =T whatever the value of bk n is, and, using (13):

π(x n >y max and y n ≤y max ) = µ v | ψ(ϕ(u n , x n-1 ), v) ≤ y max .

2. f n-1 =F: then, f n =T if and only if rf n =t and bk n =F. Thus, chosing bk n =F ensures that: rf n =t and ψ(ϕ(u n , x n-1 ), v) ≤ y max together yield y n ≤y max . Alternatively, bk n =T prevents the condition y n ≤y max from occurring. By definition of the outer probability (9), we finally get, using (13):

π(x n >y max and y n ≤y max ) = β(rf =T) × µ v | ψ(ϕ(u n , x n-1 ), v) ≤ y max , which corresponds to the probabilistic evaluation of the predicate "x n >y max and y n ≤y max " if the nondeterministic alternative bk n =F/T is interpreted as demonic [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF].

Discussion 2 (Conditioning and its variations) Conditioning is generally not considered in the field of probabilistic automata. It is, however, central in probabilistic programming, see, e.g., [START_REF] Olmedo | Conditioning in probabilistic programming[END_REF][START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF][START_REF] Tolpin | Probabilistic programs with stochastic conditioning[END_REF] for studies in which conditioning is the main subject. The observe primitive, pervasive in all tools, is used to specify posterior distributions given constraints (as we do in Definition 1). The litterature on probabilistic programming distinguishes between hard (also called deterministic) and soft (also called stochastic) conditioning [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF][START_REF] Tolpin | Probabilistic programs with stochastic conditioning[END_REF]. In the basics of probability theory, however, the only notion is that of conditional expectation [START_REF] Dellacherie | Probabilities and potentials[END_REF], from which other notions are derived, e.g., conditional probability, transition probability or stochastic kernel, and disintegration (or regular version of conditional expectation). Deriving such notions is straightforward in our case, since we restrict ourselves to discrete probability spaces. We will discuss this further when extending Bayesian networks to Mixed Systems, in Section 2.2.

Discussion 3 (consistency) Inconsistency formalizes self-contradiction, for Mixed Systems. The condition "π(Ω c ) > 0" in statement 2 of Definition 1 means that Ω c has non-empty intersection with the support of π, defined as the set of ω's of positive probability: π(ω) > 0. This simple definition for the support, which is only valid for discrete probabilities, allows us to propose a simple definition for the notion of consistency. When continuous probability spaces are considered (like the Gaussian), the above definition for the support no longer holds. The right definition relies on topological properties. As a consequence, our elementary definition of consistency would no longer apply. This is next illustrated on our running example.

Example 4 [consistency] Consider model [START_REF] Abbes | True-concurrency probabilistic models: Markov nets and a law of large numbers[END_REF][START_REF] Abbes | Concurrency, sigma-algebras, and probabilistic fairness[END_REF]. Statement 2 of Definition 1 defines consistency as the existence of a state q in relation through C with an ω belonging to the support of π, which is fairly simple. Suppose, for a while, that u n , x n , y n , v n possess real domain, µ(dv) = χ(v)dv, where dv denotes the Lebesgue measure, density χ is continuous and everywhere positive, and function v → ψ(x, v) is bijective and bicontinuous for every fixed x. Then, fixing the value of y n , for a given pair (u n , x n-1 ), will fix the value of v n if f n =T in the equation defining y n . With reference to Example 3, the only difference is that a parallel composition with the statement observe y was added. So, it still makes sense to consider the two cases 1 and 2 of Example 3. In case 1, we get W = {(rf , v) | ψ(ϕ(u n , x n-1 ), v)=y n }, whence (β×µ)(W )=0. Deducing inconsistency would be nonsense, however, since the support of µ is R. This illustrates that our pedestrian definition of consistency no longer works if real variables and distributions having densities with respect to Lebesgue measure are considered.

Equivalence

In this section, we study equivalence. To this end, we introduce the following operation of compression, on top of which equivalence is defined:

Definition 2 (compression) For S = (Ω, π, X, C) a Mixed System, we define the following equivalence relation on Ω, i.e., ∼ ⊆ Ω×Ω is such that:

(ω, ω ) ∈ ∼ if and only if: ∀q ∈ Q : ωCq ⇔ ω Cq . (14)
As usual, we write ω ∼ ω to mean (ω, ω ) ∈ ∼. The compression of S, denoted by S = ( Ω, π, X, C), is then defined as follows:

• Ω is the quotient Ω/∼, which elements are written ω;

• ω Cq iff ωCq for ω ∈ ω; and

• π( ω) = ω∈ ω π(ω).
Say that S is compressed if it coincides with its compression.

Distinguishing ω and ω is impossible if ω∼ω . Equivalence is defined on top of compression (see item 1 of Definition 1 for notation C π ):

Definition 3 (equivalence) Two compressed mixed systems S and S are equivalent if they possess identical sets of variables X=X , and there exists a bijective map ϕ : C π → C π satisfying the following conditions for every pair (ω, q) ∈ Ω × Q, where (ω , q ) = def ϕ(ω, q):

ω C π q ⇔ ω C π q ; π (ω ) = π(ω) ; q = q . ( 15
)
S and S are equivalent, written S≡S , if their compressions are equivalent.

The following result expresses that mixed system equivalence preserves probabilistic semantics:

Lemma 4 Any two equivalent mixed systems, S 1 ≡ S 2 , possess identical probabilistic semantics:

π 1 = π 2 and π 1 = π 2 .

Inria

Proof: It is enough to prove the lemma in the following two cases: 1) S 1 and S 2 are both compressed, and 2): S 2 = S 1 . The result is immediate for case 1), so we focus on case 2). Let Q be the common domain of X 1 = X 2 and A ⊆ Q be a state property. Then,

π 1 (A) = π c 1 {ω 1 | ∃q ∈ A : ω 1 C 1 q} = π c 1 {ω 1 | ω 1 ∈ ω 1 and ∃q ∈ A : ω 1 C 1 q} = π c 1 { ω 1 | ∃q ∈ A : ω 1 C 1 q} = π 1 (A) = π 2 (A) .
A similar proof holds for inner probabilities.

Discussion 4 (equivalence) Floyd/Hoare/Dijkstra logic of pre-and postconditions for imperative languages was extended to encompass probability and nondeterminism with pGCL (probabilistic Guarded Command Language) [START_REF] Kozen | Semantics of probabilistic programs[END_REF][START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF][START_REF] Mciver | Abstraction, Refinement and Proof for Probabilistic Systems[END_REF][START_REF] Katoen | Understanding probabilistic programs[END_REF][START_REF] Olmedo | Conditioning in probabilistic programming[END_REF][START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF]. The semantics is defined as the probability of weakest preconditions under demonic nondeterminism. McIver-Morgan notions of refinement and equivalence follow from this semantics. This approach is also used to define equivalence of probabilistic programs, see, e.g., Section 3.1 of [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF].

As pointed in Discussion 1, the above semantics parallels our consideration of outer/inner probabilities in point 3 of Definition 1. Compared to McIver-Morgan notion of equivalence, the notion of equivalence we propose in Definition 3 is more basic and direct. It implies equivalence of the evaluation of state properties using outer/inner probabilities.

Marginal

For (X, Y ) a pair of random variables with joint distribution P (x, y), the distribution of X is given by the marginal of P , namely: P (x) = def y P (x, y). We extend this notion to Mixed Systems, by viewing it as a hiding operation, see Figure 2. For C ⊆ Ω × Q a relation where Q is the domain of tuple X, Y ⊆ X a subset of variables, and Even if S was itself compressed, due to the projection of relation C, the Mixed System defining the marginal in Definition 5 may require a compression.

Q C (Ω, π) y x

Z = X -Y , we denote by

Pr Y : 2 Ω×Q → 2 Ω×Q Y : Pr Y (C) = def {(ω, q Y ) | ∃q Z : ωC(q Y , q Z )} the projection of C over Y .
Example 5 [Link with the classical notion of marginal for probabilities] Let us apply Definition 5 to the purely probabilistic system of Example 2, namely S proba = (Q, π, {X, Y }, diag) , having two variables X, Y , corresponding state space Q, and Ω = Q with C = diag, the diagonal. This is the model of a pair (X, Y ) of visible variables with joint probability distribution π(x, y), where x and y denote values for X and Y , respectively. The projection of diag on Y is

Pr Y (diag) = {(x, y, y ) | y = y } .
Thus, (x, y) ∼ (x , y ) if and only if y = y . Thus, when using the formula of Definition 5 to define Margin Y (S proba ), the private probability space (Q, π) must be compressed as π(y) = x π(x, y), showing that our notion of marginal boils down to the classical notion for probabilities in this case.

Parallel composition

Mixed Systems are equipped with a parallel composition: common state variables are unified (thus causing synchronization constraints); on the other hand, probabilistic parts remain local and independent, conditionally to the satisfaction of synchronization constraints. This is illustrated on Figure 3.

y 1 y 2 (Ω 1 , π 1 ) × (Ω 2 , π 2 ) x y 1 y 2 C 1 ∧ C 2 Q = dom(x, y 1 , y 2 ) ↑ factor graph ← formulas (18) C 1 (Ω 1 , π 1 ) Q 1 x x Q 2 C 2 (Ω 2 , π 2 )
Figure 3: Illustrating the parallel composition, for y 1 , y 2 local variables and x shared. The factor graph, capturing the connection via identical wires, is depicted on the top in black; the definition using formulas ( 18) is shown in blue.

Formally, let I be a finite set, and, for each i∈I, let X i be a finite set of variables with domain Q i , and set X = i∈I X i with domain Q. Say that tuple (q i ) i∈I is compatible, written

i∈I q i , (16)
if q i (x) = q j (x) for any pair (i, j) of indices and every shared variable x ∈ X i ∩ X j . If i∈I q i , their join

i∈I q i ∈ Q (17)
is defined by i∈I q i (x) = q i (x) whenever x ∈ X i .

Inria

Definition 6 (parallel composition and Factor Graph) The parallel composition S 1 S 2 of two mixed systems S 1 and S 2 is the Mixed System S such that:

X = X 1 ∪X 2 , Ω = Ω 1 ×Ω 2 , π = π 1 ×π 2 (cartesian product), and C = (ω 1 , ω 2 ), q 1 q 2 | q 1 q 2 and ω 1 C 1 q 1 and ω 2 C 2 q 2 , (18)
We attach to parallel composition S = i∈I S i its Factor Graph G S , which is a nondirected bipartite graph whose set of vertices collects systems and variables:

S i | i ∈ I ∪ x | x ∈ i∈I X i ,
and G S has edges (S i , x), for i ∈ I and x ∈ X i , also denoted by S ix.

The composition of two consistent systems may be inconsistent. Let

nil = ({1}, δ 1 , ∅, {(1, )}) (19)
be the nil system, with trivial probability space (Ω, π) = ({1}, δ 1 ) and no visible variable; its state space is the singleton Q nil = { } where is some distinguished element, and its relation is the singleton C = {(1, )}. The nil system is neutral for parallel composition: nil S ≡ S holds, for every S.

Factor Graphs obey the following rule, where ∪ denotes the union of graphs:

G S1 S2 = G S1 ∪ G S2 . (20)
The associativity and commutativity of this parallel composition is immediate, as it is directly inherited from the same properties satisfied by the Cartesian product of probability spaces and the conjunction of relations. Factor Graphs and the parallel composition of Mixed Systems are useful in decomposing large but sparse systems, into a parallel composition of smaller, locally interacting, subsystems.

Lemma 7 S 1 ≡ S 1 implies S 1 S 2 ≡ S 1 S 2 , expressing that parallel composition preserves equivalence.

See Appendix A.2 for the proof.

Bayesian Calculus and Bayesian Networks

So far Factor Graphs and related algorithms are able to capture joint distributions relating different statistical data, but they cannot capture causality, as argued by Judea Pearl [START_REF] Pearl | Causality[END_REF]. Actually, Judea Pearl states that causality requires extra, structural, information that must be added to the specification of probability distributions: directed graphs are used to this end. Another issue is that of incremental sampling of a compound system: whereas the sampling of a parallel composition is generally global (or using the sophisticated iterative methods used, e.g., in [START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF]), one could ask whether it could be performed incrementally.

In statistics based on graphical models, these questions are answered by considering, in addition to Factor Graphs, so-called Bayesian Networks [START_REF] Pearl | Fusion, propagation, and structuring in belief networks[END_REF]. Bayesian networks specify causality information by means of directed graphs, which bring the extra information advocated by J. Pearl to talk about caussality. Bayesian networks also naturally support incremental execution. In this section, we show how these concepts supporting causality and incremental sampling, can be extended to Mixed Systems.

As a preamble, we recall some facts from basic probability theory. For a pair (X, Y ) of random variables with joint distribution P (x, y), usual Bayes formula writes P (x, y)=P (y)P (x|y), where P (y) = def

x P (x, y) is the marginal distribution of Y and P (x|y) is the conditional distribution of X given that Y =y, assigning, to each value y of Y , a probability for X. Sampling P (x|y) consists in 1) nondeterministically selecting a value for y, and then 2) with this value of y, sampling X according to P (x|y). P (x|y) is called a transition probability, or a probability kernel or stochastic kernel, depending on the contexts and communities: y → P (x|y) maps any value for Y to a probability distribution for X. We now extend these notions to Mixed Systems.

Mixed Kernel

We begin by extending the notion of probability kernel to that of Mixed Kernel. The starting idea consists in defining a Mixed Kernel as a function, mapping every Y -state of a set Y of variables, to a system having X as its set of variables. For the notations used in the sequel, the reader is referred to the beginning of Section 2.

Definition 8 (Mixed Kernel) A Mixed Kernel (or simply kernel) is a map

K : Q X → S(X ) ,
where X and X are two finite sets of variables such that X ∩ X = ∅, called the sets of inputs and outputs of kernel K. In the sequel, we shall denote these two sets X and X by X in K and X out K , respectively. The probabilistic semantics of K is the pair of maps

q in → π(q in ), π(q in ) (21)
where q in is a value for the input variables X in K , and π(q in ) and π(q in ) are the outer and inner probabilities associated to Mixed System K(q in ).

For q∈Q and C ⊆ Ω×Q, we write

C q = def {ω∈Ω | ωCq}, and C ω = def {q∈Q | ωCq} . ( 22
)
Convention 1 A kernel K whose input set X is empty identifies with the Mixed System S = K( ) it defines, where Q X is the singleton { }. Vice-versa, any system S identifies with the kernel K whose input set X is empty and K( ) = S.

Bayesian Network

Definition 9 (Bayesian Network) Let N =(X ∪ K, →) be a directed acyclic bipartite graph, where X and K are finite sets of variables and Mixed Kernels, and → ⊆ (X×K) ∪ (K×X) is the set of edges. For K ∈ K, we denote by • K and K • the sets of variables x ∈ X such that x → K and K → x, respectively. N is called a Bayesian Network if satisfies the following conditions:

∀K ∈ K =⇒ X in K ⊆ • K and X out K = K • . ( 23
)
∀K 1 , K 2 ∈ K, K 1 = K 2 =⇒ K 1 • ∩ K 2 • = ∅ (24)
For convenience, we will denote by

K 1 ; K 2 (25)
Inria a Bayesian network N =(X∪K, →) whose set K contains only two Mixed Kernels K 1 and K 2 , such that

K 1 → K 2 and X = X in K1 ∪X out K1 ∪X in K2 ∪X out K2 .
This notion is illustrated on Figure 4 for two Mixed Kernels communicating via variable x (compare with Figure 3).

y 1 y 2 C 1 (Ω 1 , π 1 ) Q 1 x x Q 2 (Ω 2 , π 2 ) C qx 2 Figure 4: Bayesian Network S 1 ; K 2 . Mixed Kernel K 2 has input x.
To Bayesian Network N =(X∪K, →), we associate the partial order (X∪K, ), where is the transitive closure of →. In the following definition, for q a valuation of the set X of variables and K a kernel belonging to K, q ↓ • K and q ↓K • denote the restriction of q to the variables belonging to • K and K • , respectively. Definition 10 (incremental sampling and probabilistic semantics) The incremental sampling of Bayesian Network N is defined by structural induction over as follows:

1. Initial condition: we assume a value for every variable x ∈ min(X ∪ K), where min refers to ; we set X -= min(X ∪ K) ∩ X and K -= ∅;

2. Induction hypothesis:

X -∪ K -⊆ X ∪ K is a downward closed subset of vertices of N such that (a) K • -⊆ X -; (
b) every variable x ∈ X -holds a value, whereas every x ∈ X -does not; 3. Induction step: while X -=X, do:

(a) let K * ⊆ K-K -collect the kernels K such that • K⊆X -and K • =∅;
(b) for every K∈K * , every variable belonging to • K holds a value, hence we can sample Mixed System K(q• K ), which returns a value for q K • ;

(c) doing this for all K∈K * yields a value for every variable belonging to

X -∪ K * • ⊃ X - (the inclusion is strict); (d) set K -:= K -∪ K * and X -:= X -∪ K * •
and return to 3.

Done.

Sampling N thus returns a value q ∈ Q X for every variable belonging to X, we denote this by N q. The probabilistic semantics of N is the map q → π(q), associating to every q∈Q X such that N q, its probabilistic score

π(q) = K∈K π K, q ↓ • K q ↓K • . (26)
In [START_REF] Dempster | Upper and lower probabilities induced by a multivalued mapping[END_REF], π(K, q ↓ • K )(q ↓K • ) is the score assigned to state q ↓K • by the outer probability associated to mixed system K(q ↓ • K ).

Since inclusion X -∪ K * • ⊃ X -in step 3c is strict, the inductive procedure terminates in finitely many steps. Note that, by [START_REF] Benveniste | The synchronous languages 12 years later[END_REF], there is no need to consider π(q). The inductive procedure of Definition 10 is formalized in Algorithm 1.

Algorithm 1 Incremental sampling of Bayesian Network N Require: ∀x ∈ min(X ∪ K), x is defined Ensure: ∀x ∈ X, x is defined X -← X ∩ min(X ∪ K) and K -← ∅ while X -=X do K * ← { K | • K⊆X -and K • =∅ } for all K∈K * do sample(K(q ↓ • K )) end for end while K -← K -∪ K * X -← X -∪ K * •
Definition 11 (Bayesian network equivalence) Let N 1 and N 2 be two Bayesian networks such that X 1 = X 2 . Say that N 1 and N 2 are probabilistically equivalent, written N 1 ≡ P N 2 , if they possess equal probabilistic semantics:

π 1 = π 2 .
By Lemma 4, S ≡ S implies S ≡ P S , when regarding mixed systems S and S as Bayesian networks.

Example 6 [Finite Markov chain as a Bayesian Network] Recall that a finite sequence of random variables X 1 , X 2 , . . . , X n is called a Markov chain if the joint distribution of (X 0 , X 1 , . . . , X n ) factorizes as π(X 0 =x 0 , . . . , X n =x n ) = µ(x 0 ) n i=1 P (x i |x i-1 ), where probability µ over X, the state space of the Markov chain, is the initial condition and P (x |x) is the transition kernel, i.e., for x fixed, x → P (x |x) is a probability over x . Markov chains are thus a particular case of the Bayesian Networks proposed in Definition 9.

We next extend, to mixed systems, the notion of conditional distribution. To this end, we will use the following notation: for Y a set of variables and

q Y ∈ Q Y , (Y =q Y ) (27)
denotes the Mixed System defined as follows: Ω is the singleton {1} with trivial probability on it, Y is the set of variables, and

C = {(1, q Y )} is a singleton, expressing that Y is constrained to take the value q Y .
Definition 12 (conditional) Let S = (Ω, π, X, C) be a Mixed System, and let Y ⊆ X be a subset of variables. The conditional of S on Y , denoted by Cond Y (S), is the kernel defined by

Cond Y (S) (q Y ) = def ( Y =q Y ) S.
Link with the classical notion: Consider the following particular case for S: Ω=Q, and C is the diagonal of Ω×Q. Then, S specifies the joint distribution π for tuple X of random variables. Decompose X = Y ∪Z where Y ∩Z = ∅. Compressing Margin Y (S) yields the marginal distribution of Y . Compressing (Y =q Y ) S yields the conditional distribution π(q Z |q Y ). Therefore, Definitions 5 and 12 extend the notions of marginal and conditional existing on purely probabilistic systems.

Inria Discussion 5 (more on conditioning) When probability and nondeterminism are blended, the notion of Mixed Kernel serves the same purpose as soft or stochastic conditioning [START_REF] Tolpin | Probabilistic programs with stochastic conditioning[END_REF], since it implements the stochastic conditioning p(x | y ∼ D) discussed in the introduction of [START_REF] Tolpin | Probabilistic programs with stochastic conditioning[END_REF].

Generally, sampling the parallel composition S 1 S 2 yields a result which differs from the incremental sampling of S 1 ; Cond X1 (S 2 ) (by Convention 1 we can regard S 1 as a kernel and consider this incremental sampling). Nevertheless, the following result holds (see Definition 3 regarding isomorphic samplings):

Theorem 13 (Bayes formula) Let S = (Ω, π, X, C) be a Mixed System and Y ⊆ X a subset of variables. Then, the following Bayes formula holds:3

S ≡ P Margin Y (S) ; Cond Y (S) .
Proof: See Appendix A.3 for the proof.

The right hand side of Bayes' formula is illustrated on Figure 5. By Definition 6, parallel composition S = S∈S S defines a Factor Graph G S , having nondirected bipartite edges Sx, for every S ∈ S and every visible variable x of S. Message passing algorithms transform certain Factor Graphs associated to a parallel composition of several Mixed Systems, to Bayesian Networks while preserving the sampling. This provides such Factor Graphs with an incremental sampling: Theorem 14 (message passing algorithm) If Factor Graph G S of system S is a tree, we can transform it to a Bayesian Network N S while preserving its probabilistic semantics.

marginal: hiding X conditional: kernel with input Y hide Q C (Ω, π) Y X ; Q C (Ω, π) X Y

See Appendix A.4 for a proof.

Message passing algorithms for computing generalized likelihoods. The purpose of probabilistic languages [START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF][START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF][START_REF] Gordon | Probabilistic programming[END_REF] is not only (actually, not so much) sampling, but rather estimation/inference. Of course, in addition to performing incremental sampling, Bayes' formula also allows evaluating probabilities of properties incrementally. Then, a counterpart of Bayes' formula exists for performing maximum likelihood estimation incrementally-it is known in the pattern recognition literature as the Viterbi algorithm [START_REF] Forney | Maximum-likelihood sequence estimation of digital sequences in the presence of intersymbol interference[END_REF][START_REF] Rabiner | An introduction to hidden markov models[END_REF]. Theorem 14 shows that message passing algorithms also allow for an incremental evaluation of generalized likelihoods.

The ReactiveBayes minilanguage

In this section, we use the model of Mixed Systems to specify the semantics of the informal language we used in the introduction when discussing our running example. To make this precise, we formalize this informal language through the "ReactiveBayes" syntax presented hereafter.

To prevent from decidability issues in constraint solving, domains of variables and random variables are all assumed finite. Finally, to simplify our presentation of the syntax, domains are omitted.

Syntax

Here is the syntax, where keywords are highlighted in blue:

e ::= c | x | (e, e) | op(e) | f (e) | pre x | init x = c S ::= x ∼ P (e) | e = e | observe x | S S (28)
• An expression e is a constant c, a variable x, an external operator application op(e), a function application f (e), or a delayed version pre x for the variable x. Initial condition init x = c is required whenever pre x occurs in the program; it fixes the initial value for x.

• A Mixed System S is the declaration of a prior distribution P (e) for variable x, thus making it random; distribution P (e) has, optionally, parameters set by expression e, an equation e = e, the declaration that variable x is actually observed, or the parallel composition thereof. For each term P we assume a semantics denoted by π P , which is a probability.

No provision is given by syntax [START_REF] Den Hartog | Verifying probabilistic programs using a hoare like logic[END_REF] for writing equations relating systems. In particular, fixpoint equations S = S S cannot be expressed: ReactiveBayes does not offer full recursion. However, statements pre and init provide a limited form of recursion, supporting dynamical systems. This will be made clear in Section 3.2, where the semantics of full ReactiveBayes will be given.

Semantics

We now give the semantics of the static fragment of ReactiveBayes, namely ignoring in (28) the statements pre and init. [[S]] denotes the semantics of ReactiveBayes program S:

(i) [[observe x]] = (•, •, {x}, x = c) (ii) [[x ∼ P ]] = (Ω x , π P , {x}, x = ω x ) (iii) [[x ∼ P (e)]] = c → [[x ∼ P (c)]], where c = e (iv) [[e = e ]] = (•, •, vars(e) ∪ vars(e ), e = e ) (v) [[S 1 S 2 ]] = [[S 1 ]] [[S 2 ]] (29)

Inria

In (i), the semantics has no probabilistic part, and a single visible variable x whose value c is given, but left unspecified. In (ii), probability distribution P is fixed; the semantics consists of the probability space (Ω x , π P ), where Ω x is a private copy of the domain of x equipped with probability π P and having generic element ω x ∈ Ω x ; equation x = ω x exposes ω x for further interactions through x. In (iii), the probability depends on an expression e, whose generic value is denoted by c; the semantics is the kernel mapping c to [[x ∼ P (c)]]. Line (iv) defines the semantics of equations; "vars(e)" denotes the set of variables involved in expression e; the semantics has no probabilistic part. Finally, (v) makes this semantics structural. Thanks to formula [START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF] of Definition 6, it also defines the Factor Graph representing S.

The following fragment of ( 29) is mapped to a Bayesian Network. In the following formulas, N [[S]] denotes the Bayesian Network defined by S, when it exists:

(i) N [[observe]] = {is_source(x)} (ii) N [[x ∼ P ]] = {x} (iii) N [[x ∼ P (e)]] = vars(e) → [[x ∼ P (e)]] → x (iv) N [[x = e]] = vars(e) → [[x = e]] → x (v) N [[S 1 S 2 ]] = N [[S 1 ]] ∪ N [[S 2 ]] (30)
In (i), is_source(x) denotes x flagged with the condition that it must remain a source node in any of its environments. Application of Rule (v) is subject to the following success conditions:

Condition 1 (success conditions)

1. The union N [[S 1 ]] ∪ N [[S 2 ]
] possesses no circuit and satisfies the conditions of Definition 9, and 2. The result keeps satisfying all inherited conditions (i).

These conditions ensure that parallel compositions are incremental. The message Passing algorithm presented in Theorem 14 allows source-to-source rewriting for mapping tree shaped non-directed Factor Graphs to directed Bayesian Networks.

Example 2

The following picture displays, on the top, the Factor Graph associated to S 1 S 2 S 3 S 4 , and, on the bottom, the Bayesian Network resulting from applying the message passing algorithmfor better readability we show only shared variables:

y n S 2 f n S 1 v n S 3 S 4 Cond y (S 4 ) ↑ y n ↑ Cond f (S 3 ) ← f n ← S 1 → v n → Cond v (S 2 )
where

S 1 = def S 1 Margin v (S 2 ) Margin f (S 3 ) Margin y (S 4 ).
Discussion 6 (if-then-else) In Example 1, system S 1 involves an "if-then-else" statement. Syntax (28), however, does not involve such statements. This means that "if-then-else" statements are seen by syntax [START_REF] Den Hartog | Verifying probabilistic programs using a hoare like logic[END_REF] as one instance of "f ", to which no particular attention is paid. The semantics of this "f " obviously depends on the value of the Boolean control signal. However, neither the factor graph, nor the Bayesian network associated to S 1 , depend on which branch is active in this "if-then-else" statement. This is harmless if the focus is on modeling. Considering "if-then-else" and paying attention to it is definitely needed in probabilistic reasoning [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF], see Appendix A.1. The same holds when performing inference or learning [START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF]; see also the discussion of objective 3 of probabilistic programming on page 5.

So far we have presented models involving no dynamics. In the next section we move to our proposed formal model for dynamical systems: Mixed Automata.

Mixed Automata

The idea is simple: we upgrade notions, from automata, to Probabilistic Automata, and to Mixed Automata:

1. Transitions q α -→ q , where q and q are states and α is an action, correspond to automata.

Upgrading them to q

α -→ π q , where π is the next probabilistic state and denotes probabilistic sampling, yields Simple Probabilistic Automata following Segala and Lynch [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Lynch | Compositionality for probabilistic automata[END_REF].

3. Upgrading them further to q α -→ S q , where S is a Mixed System and denotes sampling, yields Mixed Automata.

Definition and properties

The formal definition is introduced next. It uses the notation S(X), introduced at the end of Definition 1. We assume an underlying alphabet Σ of actions.

Definition 15 (Mixed Automaton) A Mixed Automaton is a tuple M = (Σ, X, q 0 , →), where: Σ ⊆ Σ is a finite set of actions, X is a finite set of variables having domain Q = x∈X Q x , q 0 ∈ Q is the initial state, and → ⊆ Q×Σ×S(X) is the transition relation. We write q α -→ S (or q α -→ M S when we wish to make M explicit) to mean (q, α, S) ∈ →. We require that M shall be deterministic:

for any pair (q, α) ∈ Q×Σ, q α -→ S and q α -→ S implies S=S . ( 31
)
The sampling of M is its set of runs r, which are finite sequences of chained transitions:

r = q 0 α1 -→ S 1 q 1 α2 -→ S 2 q 2 . . . q k-1 α k -→ S k q k , (32)
where Mixed Systems S 1 , . . . , S k are consistent, and S q is the sampling introduced in Definition 1.

The transitions of Mixed Automata target Mixed Systems, which combine nondeterminism with probabilities. Therefore, Mixed Automata capture nondeterminism despite Condition [START_REF] Gerhold | Model-based testing of probabilistic systems[END_REF].

Inria

Example 7 [comparing with classical notions] Let (X n ) n≥0 be a Markov chain with state space Q, initial state q 0 , and transition probability P (q | q). We can reformulate it as the Mixed Automaton M = (Σ, X, q 0 , →), where: Σ is the singleton {α}; variable X has domain Q; → maps (q, α) to the purely probabilistic Mixed System of Example 2, representing probability q → P (q | q) for given state q.

Like automata and Probabilistic Automata, Mixed Automata come equipped with a notion of parallel composition, built on top of the parallel composition of Mixed Systems. The simplest idea is that the transitions of parallel composition M 1 M 2 will take the form q 1 q 2 α -→ S 1 S 2 q 1 q 2 , where q 1 q 2 and S 1 S 2 are defined in [START_REF] Borgström | A lambdacalculus foundation for universal probabilistic programming[END_REF] and Definition 6, respectively. In this simple construction, synchronizing the two transitions is by having them perform the same action α.

To be able to define the semantics of our ReactiveBayes minilanguage, we will, however, need the more flexible synchronization mechanism of "compatible actions"-this is known to be only a technical extension. We thus assume that the underlying alphabet Σ of actions is equipped with a commutative and associative join partial operation Σ : Σ × Σ → Σ, where α 1 Σ α 2 is defined whenever the two actions are compatible, written α 1 Σ α 2 . In the composition of Mixed Automata, the components synchronize on compatible actions and move to the parallel composition of target systems by performing the join of the two actions: Definition 16 (parallel composition) Let M 1 and M 2 be two Mixed Automata having compatible initial states q 0,1 q 0,2 . Their parallel composition M 1 M 2 has alphabet Σ 1 ∪Σ 2 , set of variables X 1 ∪X 2 , and initial state q 0,1 q 0,2 . Its transition relation -→ M is the minimal relation satisfying the following condition, where S 1 S 2 was defined in Definition 6:

q i αi -→ Mi S i for i = 1, 2 q 1 q 2 and α 1 Σ α 2 =⇒ q 1 q 2 α -→ M S 1 S 2 , where α = α 1 Σ α 2 .
The next important notion is that of (bi)simulation, which is central in automata theory. We upgrade it, from the basic notion for automata up to the extended notion for Mixed Automata:

1. In the context of automata, relation ≤ on pairs of states is a simulation if it satisfies [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF]:

q 1 α -→ q 1 q 1 ≤ q 2 =⇒ ∃q 2 : q 2 α -→ q 2 q 1 ≤ q 2
2. This definition is upgraded to Probabilistic Automata as follows [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF]:

q 1 α -→ π 1 q 1 ≤ q 2 =⇒ ∃π 2 : q 2 α -→ π 2 π 1 ≤ P π 2
where ≤ P is the lifting of ≤ to pairs of probabilistic states. We have: π 1 ≤ P π 2 ensures, for each q 1 such that π 1 q 1 , the existence of q 2 satisfying π 2 q 2 and q 1 ≤ q 2 . (

) 33
3. This definition will be further upgraded to Mixed Automata as follows:

q 1 α -→ S 1 q 1 ≤ q 2 =⇒ ∃S 2 : q 2 α -→ S 2 S 1 ≤ S S 2 (34)
where ≤ S is the lifting of ≤ to pairs of Mixed Systems. We request:

S 1 ≤ S S 2 shall ensure, for each q 1 such that S 1 q 1 , the existence of q 2 satisfying S 2 q 2 and q 1 ≤ q 2 . (

) 35
Such a lifting is introduced next. Let S 1 and S 2 be two Mixed Systems.

Definition 17 (lifting relations on Mixed Systems states) Let ρ ⊆ Q 1 ×Q 2 be any state relation. Mixed System relation ρ S ⊆ S(X 1 )×S(X 2 ) is the lifting of ρ if there exists a weighting function w : Ω 1 ×Ω 2 → [0, 1] such that:

1. For every triple (ω 1 , ω 2 , q 1 ) ∈ Ω 1 ×Ω 2 ×Q 1 such that w(ω 1 , ω 2 ) > 0 and ω 1 C 1 q 1 , there exists q 2 ∈ Q 2 such that q 1 ρ q 2 , and ω 2 C 2 q 2 ; 2. Weighting w projects to π 1 and π 2 :

ω2 w(ω 1 , ω 2 )=π 1 (ω 1 ) and ω1 w(ω 1 , ω 2 )=π 2 (ω 2 ).
By construction, this definition for the lifting of state relations to relations on Mixed Systems satisfies [START_REF] Gordon | Probabilistic programming[END_REF]. Note the existential quantifier in Condition 1. By Condition 2, w induces a probability on Ω 1 ×Ω 2 . We write S 1 ρ S S 2 to mean (S 1 , S 2 ) ∈ ρ S .

Discussion 7 (lifting and coupling) Our lifting is a direct extension of the technique used in [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF] for Probabilistic Automata. In the context of probabilistic reasoning, the same technique was also extensively studied under the name of probabilistic coupling [START_REF] Barthe | Relational reasoning via probabilistic coupling[END_REF][START_REF] Hsu | Probabilistic couplings for probabilistic reasoning[END_REF]. Weighting function w(ω 1 , ω 2 ) of Definition 17 transposes probabilistic coupling to our model of Mixed Automata in which nondeterminism and probability are combined. In a different community, "stochastic nondeterminism" was extensively studied through the notion of Non-deterministic labelled Markov process in [START_REF] D'argenio | Bisimulations for nondeterministic labelled markov processes[END_REF][START_REF] Doberkat | Stochastic non-determinism and effectivity functions[END_REF], in a categorical framework; the second reference encompasses continuous distributions (beyond discrete).

Lemma 18 S 1 ρ S S 2 and S 1 ≡S 1 together imply S 1 ρ S S 2 .

See Appendix B.1 for a proof.

Definition 19 (simulation) Given two Mixed Automata M 1 , M 2 , we say that M 2 simulates M 1 , written M 1 ≤M 2 , if they possess a simulation, i.e., a relation ≤ ⊆ Q 1 ×Q 2 such that q 0,1 ≤q 0,2 and, for every pair q 1 ≤q 2 and every transition q 1 α -→ 1 S 1 , there exists a transition q 2 α -→ 2 S 2 such that S 1 ≤ S S 2 , where ≤ S denotes the lifting of ≤. M 1 and M 2 are called simulation equivalent if they simulate each other. M 1 and M 2 are called bisimilar if there exists a relation ∼ ⊆ Q 1 ×Q 2 such that both ∼ and its transpose are simulations. Discussion 8 (simulation equivalence vs. bisimilarity) Despite the condition (31) that the transition relation shall be deterministic, the two notions of " 'simulation equivalence" and "bisimilarity" differ. The reason is that nondeterminism is hidden behind the Mixed Systems targeted by transitions. Actually, we will prove in our forthcoming Theorem 22 that Segala's Probabilistic Automata [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Lynch | Compositionality for probabilistic automata[END_REF], which possess nondeterministic transition relations, can be embedded into Mixed Automata while preserving simulations.

The notion of simulation and its derived constructs are the core topic of the literature on automata and their probabilistic extensions. The reader is referred to the next section for a bibliographical discussion.

Lemma 20 Parallel composition preserves simulation

: M 1 ≤M 1 and M 2 ≤M 2 together imply M 1 M 2 ≤ M 1 M 2 .
Inria See Appendix B.2 for a proof. Discussion 9 (Mixed Automata are causal in time) Mixed Automata remain a causal model in time, since the current transition depends on the past, not on the future. Consequently, Mixed Automata cannot be used to specify acausal estimation problems, e.g., estimating unmeasured variable z k based on observations of X 0 , . . . , X k , . . . , X N . To perform this, we must "unfold time as space", i.e., regard X 0 , . . . , X N as a (N +1)-tuple of variables, not as successive occurrences in time of variable X. Note that the transition relations of Mixed Automata inherit, from Mixed Systems, the Bayesian Calculus and the notions of Factor Graph and Bayesian Network.

Mixed Automata for the semantics of ReactiveBayes

In this section we first give the semantics of the full ReactiveBayes minilanguage (28) in terms of Mixed Automata. Recall that the semantics of the static part of the language was given in (29,(i)-(v)).

Notations: To every variable x, we associate its successive previous versions • x, •2 x, •3 x, . . . , where

•(n+1) x = def • ( •n x) and Q• x = Q x . (36)
Then, we define

• e(x) = def e( • x) (37)
as being the expression e in which every variable x is replaced by its previous version • x. We will use the Mixed System (x=q x ), defined in [START_REF] Dempster | A generalization of bayesian inference[END_REF]: this system has trivial probabilistic part, variable x, and enforces the value q x for it. We begin with delay pre and initialization init:

(vi) [[pre x]] = {t} , {x, • x} , -, {q t -→ ( • x=q x ) | ∀q ∈ Q} (vii) [[init x = c]] = {t} , {x} , c , c t -→ nil and t -→ nil (38)
The semantics of pre is stated in (vi). It is the Mixed Automaton with trivial action alphabet (singleton {t}), two variables x (receiving the current value) and • x (delivering the previous value), an undefined initial state, and the set of transitions

q t -→ ( • x = q x ) ,
where q ranges over the set of all states and q x is the x-coordinate of q-this transition relation formalizes the constraint that (pre x) n holds the value of x n-1 .

Since the initial state is undefined in the delay statement, a specification of the initial value is required, by using initialization statement init. Its semantics is stated in (vii), where nil is the trivial Mixed System defined in [START_REF] Bruni | Bayesian network semantics for petri nets[END_REF]. This Mixed Automaton possesses x as its only variable, c ∈ Q x as its initial state, and otherwise does nothing, i.e., sets no constraint on its environment. So far we have completed the semantics of ReactiveBayes as defined in [START_REF] Den Hartog | Verifying probabilistic programs using a hoare like logic[END_REF], for which actions were not used-only the trivial "true" action was used in the semantics. Since Mixed Automata is a richer framework, it can support the following richer language involving state machines, by adding the following syntax, with reference to (28):

Actions α are previous versions of expressions of Boolean type. In the additional statement "on α then S else S", actions α and ¬α trigger the transition leading to the first and second system, respectively. If α is the constant "true", we simply write S instead of "on true then S".

We now give the corresponding semantics (t denotes the Boolean value "true", and we refer the reader to Definition 1 regarding nil and the distinguished state ):

(viii)
[[on α then S else S ]] = S and S have previous state p

   {α, ¬α} , X ∪ X , • p α -→ S, p ¬α -→ S    (ix) [[A 1 A 2 ]] = [[A 1 ]] [[A 2 ]] (40)
The right hand side of (viii) is an inference rule meaning "numerator entails denominator ". By [START_REF] Halmos | Measure Theory. Graduate Texts in Mathematics[END_REF] and the syntax for actions in [START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF], action α in (viii) is evaluated by using the previous state p. At a given instant, the previous state is known, and can thus be used as the source state of the two transitions. The initial state is left unspecified. Focus on the parallel composition (ix).

With reference to Definition 16, we now formalize the compatibility relation Σ and the join operator Σ :

α 1 Σ α 2 always holds, and α 1 Σ α 2 = def α 1 ∧ α 2 . ( 41
)
4 Comparison with Segala's Probabilistic Automata Probabilistic Automata (pa) [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Lynch | Compositionality for probabilistic automata[END_REF] were originally proposed by Segala and Lynch. To simplify our comparison, we discuss here the version of pa with no consideration of internal actions.

According to the classification made by Sokolova and de Vink [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF], we study the link with both the Simple (Segala) Probabilistic Automata and the (Segala) Probabilistic Automata. For the former, actions are selected and then a transition to a probabilistic state is selected nondeterministically. For the latter, both the action and a state are jointly selected, probabilistically. This distinction is referred to as reactive vs. generative models in [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF]. Simple Probabilistic Automata existed way before the work of Segala and Lynch [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Lynch | Compositionality for probabilistic automata[END_REF], in the community of applied mathematics and probability theory, where they are known under the name of Markov Decision Processes (MDP) [START_REF] Bellman | A markovian decision process[END_REF][START_REF] Martin L Puterman | Markov decision processes: discrete stochastic dynamic programming[END_REF]. In this context, the main considered problem is the synthesis of an optimal policy to minimize some expected cost function on trajectories of the system. The minimization is over scheduling policies, which are causal rules for selecting the next action given the past trajectory. Once this policy has been fixed, the resulting dynamics is a Markov Chain. Studies on (bi)simulation were more recently developed for MDP's [START_REF] Givan | Equivalence notions and model minimization in markov decision processes[END_REF], and further developed to support robustness by defining metrics between finite MDP's [START_REF] Ferns | Bisimulation metrics for continuous markov decision processes[END_REF].

In the following, P(Q) denotes the set of all probability distributions over the set Q. Formally, we consider a tuple P = (Σ, Q, q 0 , →), where Σ is the finite alphabet of actions, Q is a finite state space, q 0 ∈Q is the initial state, and the probabilistic transition relation → is defined in two different ways:

Simple Probabilistic Automaton (spa) : → ⊆ Q×Σ×P(Q) (42)
Probabilistic Automaton (pa) : → ⊆ Q×P(Σ×Q)

Inria

In the following definitions, relation ≤ P is the lifting, to probability distributions over Q×Q , of the relation ≤ over Q×Q -for the definition of the lifting ≤ P , the reader can use Definition 17 adapted by ignoring relations C 1 and C 2 .

Details for spa, model

We write q α -→ P µ to mean (q, α, µ) ∈ → and µ q to mean that sampling µ returns next state q . The sampling is: if P is in state q∈Q, performing α∈Σ leads to some target set of probability distributions over Q, of which one is selected, nondeterministically, and used to draw at random the next state q . A simulation relation is a relation ≤ ⊆ Q×Q such that, for any q ≤ q , the following holds: if q α -→ P µ, there exists µ such that q α -→ P µ and µ ≤ P µ . The parallel composition of spa [START_REF] Lynch | Compositionality for probabilistic automata[END_REF] is defined by:

P 1 P 2 = (Σ, Q, q 0 , →), where Σ = Σ 1 ∪Σ 2 , Q = Q 1 ×Q 2 , q 0 = (q 0,1 , q 0,2 ), and (q 1 , q 2 ) α -→ µ 1 ×µ 2 holds iff q i α -→ i µ i for i = 1, 2.
Details for pa, model [START_REF] Kindermann | Markov random fields and their applications[END_REF] We write q -→ P µ to mean (q, µ) ∈ → and µ (α, q ) to mean that sampling µ jointly returns action α and next state q . The sampling is: P being in state q∈Q leads to some target set of probability distributions over Σ×Q, of which one is selected, nondeterministically, and used to draw at random the next pair (α, q ) of action and state. A simulation relation is a relation ≤ ⊆ Q×Q such that, for any q ≤ q , the following holds: if q -→ P µ, there exists µ such that q -→ P µ and µ ≤ P µ .

The parallel composition P = P 1 P 2 faces the following difficulty: there is a conflict between (1) the probabilistic choice of actions α 1 and α 2 in each component, and ( 2) the synchronization constraint on the pair (α 1 , α 2 ) possibly required by the parallel composition.

This difficulty does not exist if no synchronization constraint exists, e.g., if the composition of actions α = α 1 .α 2 is always defined. In this case, the parallel composition is straightforward: (q 1 , q 2 ) -→ P µ 1 ×µ 2 iff q i -→ Pi µ i holds for i = 1, 2. This kind of parallel composition does not capture synchronization, however.

In contrast, if strong synchronization is imposed, e.g., by requiring that α 1 =α 2 whenever one of the two actions is shared by the two components-this is the policy followed in our model of Mixed Automata-, then the above conflict exists. This conflict is usually resolved by adding a probabilistic scheduling policy specified through an auxiliary probability distribution, see the detailed discussion in [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF] and references therein. A typical approach to compose the two transitions q i -→ Pi µ i (α i , q i ), i = 1, 2 is the following:

• If synchronization constraint α 1 = α 2 = α happens to be satisfied, then the two transitions synchronize and (q 1 , q 2 ) leads to (α, (q 1 , q 2 )) with probability µ 1 (α, q 1 ) × µ 2 (α, q 2 ).

• If both actions α 1 and α 2 are local α i ∈ Σ 1 ∩Σ 2 , i = 1, 2, then the synchronization constraint is not violated. However, since only one action is permitted at a time in pa, one among the two transitions must be elected while the other one is freezed. This is achieved by tossing a (possibly biased) coin with parameter σ ∈ (0, 1), so that (q 1 , q 2 ) leads to (α 1 , (q 1 , q 2 )) with probability µ 1 (α, q 1 ) × σ and (q 1 , q 2 ) leads to (α 2 , (q 1 , q 2 )) with probability µ 2 (α 2 , q 2 ) × (1 -σ).

• Other cases are forbidden.

Collecting the outcomes that are not forbidden results in a transition of the form q -→ P μ (α, q ), where μ is unnormalized. A subsequent normalization is performed to get the final definition q -→ P µ (α, q ) for the transitions of the parallel composition. The definition of this parallel composition thus requires specifying an additional probability distribution (the parameter σ of the biased coin). Other variants for solving the same conflict all need such additional probability distributions-typically referred to as schedulers.

Discussion 10 (who comes first: nondeterminism or probability?)

The following question arises [START_REF] Wang | A denotational semantics for low-level probabilistic programs with nondeterminism[END_REF]: should nondeterminism be resolved prior or after probabilistic sampling? Since the selection of the performed action followed by that of one probability from a subset of P(Q) (for spas), or the selection of one probability from a subset of P(Σ×Q) (for pas) is performed prior to probabilistic sampling, both spa and pa models follow the first alternative. Our model of Mixed Automata follows a schyzophrenic approach: actions are selected first, leading to a Mixed System in which nondeterminism is resolved at last (See point 2 in Definition 1)-one can thus say that nondeterminism is resolved "first-and-last". As we shall see in our forthcoming comparison, the main difference between our model and models from the pa family is not in this "prior vs. after" issue, but rather in our handling of conditioning and parallel composition.

Comparison results

The following theorems relate spa and pa to Mixed Automata (proofs are constructive).

Theorem 21 (SPA vs. Mixed Automata)

1. There exists a mapping P →M P , from spa to Mixed Automata, preserving both simulation and parallel composition: In [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF], it is proved that spa can be embedded into pa, by simply "pushing" actions, from occurring prior to probabilistic choice to being part of probabilistic choice (in which case alternatives to emitting action α sum up to probability 1). So, it seems unnecessary to study the embeddings spa → Mixed Automata and pa → Mixed Automata separately, since mapping the second one seems sufficient. This is, however, not a good idea, since the two embeddings differ, in that parallel composition is preserved for spa but not for pa.

P 1 ≤P 2 iff M P1 ≤M P2 ,
Discussion 11 (More on comparing spa/pa and Mixed Automata) So far Theorems 21 and 22 compare spa/pa and Mixed Automata regarding the core notions of pa, namely simulation and parallel composition. Conditioning is not at all considered in pa theories-this indeed is the reason for them to have problems when handling synchronization in the parallel composition.

Inria

We do not see how factor graphs can be reflected in pa theories. In contrast, these concepts are naturally supported by our model of Mixed Automata. In addition, our model offers the classical concepts of pa theories, namely simulation and equivalence.

Other related work

So far we discussed work closely related to the different topics we covered. In this section we broaden our discussion by considering side topics relevant to our study.

Regarding semantic studies, we did not address denotational semantics-our sampling (Definition 1) is an operational semantics. By denotational semantics, we mean a mathematical characterization of the set of all traces that can be produced by the considered system. The subject was indeed addressed in core mathematical probability theory-it was not called this way-with the Kolmogorov extension theorem: this theorem gives the denotational semantics of a sequence of independent identically µ-distributed random variables as a probability space (Ω, F, π), where Ω is the set of trajectories, F the associated product σ-algebra, and π = µ N , whose existence and uniqueness follows from this extension theorem. Since the 1970's, mathematicians in probability theory gave a denotational semantics (this term was not used) to stochastic differential equations in a very general setting, see e.g, the seminal paper [START_REF] Stroock | On the support of diffusion processes with applications to the strong maximum principle[END_REF]. In our context of nondeterministic/probabilistic dynamical systems, the task was not really investigated by mathematicians, and one should rather look at the literature closer to computer science. The seminal paper by Kozen [START_REF] Kozen | Semantics of probabilistic programs[END_REF] defines two kinds of semantics of simple imperative probabilistic programs. The first semantics has finite horizon [0, S] where S is a stopping time (causally defined random time) and closely follows probability theory with its construction of probability spaces of program traces; the second semantics, advocated by the author, is more denotational, uses Scott-like techniques of continuous linear operators on a Banach space of measures, and supports infinite traces, see also [START_REF] Tix | Semantic domains for combining probability and non-determinism[END_REF][START_REF] Gordon | Probabilistic programming[END_REF]. This approach was extended in [START_REF] Jones | A probabilistic powerdomain of evaluations[END_REF][START_REF] Katoen | Understanding probabilistic programs[END_REF][START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF] in order to provide semantics to the observe statement present in most modern probabilistic programming languages. In [START_REF] Borgström | Measure transformer semantics for bayesian machine learning[END_REF], the semantics of a functional language supporting mixtures of continuous and discrete distributions and dedicated to certainly terminating programs, is specified as measure transformers, describing how the program itself propagates the distribution of the probabilistic inputs.

Major probabilistic programming languages do offer recursion [START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF][START_REF] Van De Meent | An introduction to probabilistic programming[END_REF], all of them offer while loops. These features raise the issue of possible non termination. Non terminating while loops are the essence of [START_REF] Baudart | Reactive probabilistic programming[END_REF]. We did not consider recursion in its full generality, but only under the limited form of non-terminating time-recursion, with Mixed Automata. Actually, time-recursion is the most widely used form of recursion considered in statistics and learning.

Inference and learning are the main concerns of probabilistic programming. Due to the generality of the considered models, Monte-Carlo based inference algorithms are preferred [START_REF] Borgström | A lambdacalculus foundation for universal probabilistic programming[END_REF][START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF][START_REF] Carpenter | Stan: A Probabilistic Programming Language[END_REF][START_REF] Goodman | Church: a language for generative models[END_REF][START_REF] Noah | The Design and Implementation of Probabilistic Programming Languages[END_REF]. Nondeterminism, which is supported by probabilistic languages, breaks the stationarity (or time-invariance) of the specified statistical models. This is a source of difficulties when invoking limit theorems of probability theory to support learning algorithms [START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF]. We did not consider learning in this work. Clearly, our model of Mixed Automata would face the same challenge if inference were considered. Extension of model based IOCO testing with probabilities was considered in [START_REF] Gerhold | Model-based testing of probabilistic systems[END_REF]-this is a different subject than statistical testing in the sense of [START_REF] Lehmann | Testing statistical hypotheses[END_REF].

In Section 4, we have shown that Mixed Automata subsume pa. Tutorial [START_REF] Sokolova | Probabilistic automata: System types, parallel composition and comparison[END_REF] investigates more variants of pa. We conjecture that similar results hold for these as well: mappings exist that preserve simulation but not parallel composition. Abstract Probabilistic Automata [START_REF] Delahaye | Abstract probabilistic automata[END_REF] are an interface model, aiming to support specification, not programming. In addition to parallel com-position, Abstract Probabilistic Automata offer refinement and possess Probabilistic Automata as their models, two concepts irrelevant to our study.

In our work we have considered only automata, whose dynamics is indexed by discrete time n. Equipping true concurrency models with probability was classical for some net models. Free choice (or confusion free) nets are models for which this is rather simple; since choices remain local and statically defined, it is easy to turn them into probabilistic choices. For event structures with confusion, however, this is no longer the case: concurrency interferes with choice, making the latter dynamically defined. This makes it intricate, to equip choices with probabilities while maximally preserving concurrency. First constructions were proposed in [4,[START_REF] Abbes | True-concurrency probabilistic models: Branching cells and distributed probabilities for event structures[END_REF][START_REF] Abbes | True-concurrency probabilistic models: Markov nets and a law of large numbers[END_REF][START_REF] Abbes | Concurrency, sigma-algebras, and probabilistic fairness[END_REF], based on the notion of branching cell, capturing the above difficulty. Infinite event structures are supported (with restrictions) for which the law of large numbers is proved. Drawbacks are: 1) different sequences of events corresponding to the same configuration may be given different probabilities, and 2) the overall probability is globally defined, hence no parallel composition can be proposed. A different construction was proposed for occurrence nets in [START_REF] Bruni | Concurrency and probability: Removing confusion, compositionally[END_REF][START_REF] Bruni | Bayesian network semantics for petri nets[END_REF], addressing the above drawback. The net is augmented with "negative places", thus enforcing supplementary causalities with the result of deferring choices until they become local. Through the notion of statically defined s-cell, the so augmented net can be given probabilistic choices meeting full concurrency, and parallel compositions of such nets is supported. In turn, the construction of the negative places works for finite nets only. In [START_REF] Bruni | Bayesian network semantics for petri nets[END_REF], a link of such augmented nets is established with Bayesian networks, thus providing a result similar to ours in Section 2.2. Finally, [1,[START_REF] Abbes | Synchronization of bernoulli sequences on shared letters[END_REF][START_REF] Abbes | Markovian dynamics of concurrent systems[END_REF] study trace monoids by equipping them with probabilities derived from local specifications, using analytic combinatoric techniques. As far as we know, this is the only approach supporting true concurrency with probabilistic choice and parallel composition, for infinite traces. Concurrency makes everything definitely harder.

Conclusion

We developed the model of Mixed (Probabilistic-Nondeterministic) Automata that subsumes nondeterministic automata, probabilistic automata, and graphical probabilistic models. In a Mixed Automaton, transitions are triggered by actions and map states to Mixed Systems, from which the next state is sampled.

Mixed Systems are stateless and involve no dynamics. They combine nondeterminism and probability in a simple setting, providing an elegant theory of equivalence and a parallel composition. We proposed the notion of Mixed Kernel equipped with an incremental composition. We generalized Bayes formula by extending, to Mixed Systems and Mixed Kernels, the notions of marginal and conditional probabilities. The parallel composition of Mixed Systems naturally brings a notion of graphical structure, which subsumes Factor Graphs; similarly, the incremental composition of Mixed Kernels supports an extension of Bayesian Networks. Message passing algorithms allow for transforming tree-shaped Factor Graphs to Bayesian Networks, as already known for the classical notions. To summarize, our model extends graphical probabilistic models to a framework in which nondeterminism and probabilities can be freely combined. This framework also subsumes Dempster's belief theory.

On top of Mixed Systems, we defined Mixed Automata and equipped them with a simulation and a parallel composition where probabilistic parts of systems can interact. This is in contrast to existing models of probabilistic automata, which do not support conditioning. It would make sense to develop an interface theory having Mixed Automata as models, along the lines of Abstract Probabilistic Automata [START_REF] Delahaye | Abstract probabilistic automata[END_REF]. We believe that the simplicity of Mixed Systems makes them an interesting candidate for the semantics of probabilistic programs-there is still a long way to Inria go before justifying this claim.

To avoid technicalities, we decided to restrict ourselves to the consideration of finite or denumerable probability spaces. This makes the definition of support of a probability and conditional probability straightforward. Since conditioning is the heart of our approach, relaxing this restriction is far from obvious, with a deep revisiting of the notion of consistency for Mixed Systems. In the last appendix of [START_REF] Benveniste | Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism[END_REF], we give hints for such an extension.

We did not investigate decidability and complexity issues, however, neither we paid attention to effectiveness. Handling constraints C is the first difficulty. To reason on control, we could keep solving simple (e.g., Boolean) constraints, e.g., by distinguishing, in our model syntax, if-thenelse statements. Other constraints may be abstracted by their associated directed or nondirected bipartite graph. Then, techniques such as the conditional dependency graphs of synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF] could be adapted.

We did not investigate either the design of learning and inference algorithms, a central motivation of probabilistic programming. When considering this subject, we would encounter the problem of correct Monte-Carlo sampling in learning algorithms, extensively studied in [START_REF] Hur | A provably correct sampler for probabilistic programs[END_REF]. In our context, this amounts to 1) identifying time-invariant model fragments, 2) applying limit theorems to them, and finally, 3) combining the results to derive learning algorithms for Mixed Systems or Automata models.

In this supplementary material, we first collect all the missing proofs. Then, with reference to Footnote 2, we include a short discussion of how to extend our model by relaxing the restriction that probability spaces should all be at most denumerable.

A Addendum and Proofs Regarding Mixed Systems

A.1 Comparison with imperative probabilistic programming, see Discussion 1

In this appendix, we compare our model of Mixed Systems with imperative probabilistic programming following the approach promoted by Mc Iver and Morgan [START_REF] Mciver | Abstraction, Refinement and Proof for Probabilistic Systems[END_REF][START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF]. This line of work addresses probabilistic extensions of Hoare logic for imperative programs, focusing on evaluating the probability of weakest preconditions of properties. We like to compare our approach with one aspect of this work, namely the modeling of the blending of probability and nondeterminismthis is only a minor aspect of the work of Mc Iver and Morgan, which focuses on decidability issues and computational cost of their proposed logic.

A.1.1 Demonic/angelic nondeterminism

We chosed to base our comparison on a different work in the same direction: [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF], which provides the most extensive developement on demonic/angelic blending of probability and nondeterminism in the language Apps. We do not claim to cover all aspects of Apps, since the focus of this reference is on the checking of almost sure termination using supermartingale techniques. Since our scope is more modest in this appendix, we will only develop an informal comparison based on the following example corresponding to Fig. 2 of [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF], reproduced here as Figs. 6 and7.

The program and its semantics are self-speaking. A key point here is the role of demonic and angelic nondeterminisms, and their combination in this program. Let us consider the postcondition P : x gets increased by one by performing Q 3 .

(

) 44
The question is: how do we assess P ? Under demonic choice, P is violated if there exists some branch in the nondeterministic choice under which P is violated. Under angelic choice, P is violated if for all branches in the nondeterministic choice, P is violated. Inspecting Fig. 7 shows that P is violated if and only if Q 1 is selected. Thus the probabilistic score that P is violated is 0.6-we do not use the term "probability" since P combines both probabilistic and nondeterministic features, and cannot be given a true probability. Can we cast this example into Mixed Systems?

A.1.2 Casting this example to Mixed Systems?

Consider the following attempt by defining the Mixed System S Q3 = {(Ω, π), C, {x, x }}, where:

• Ω = {Q 1 , Q 2 } and π(ω=Q 1 ) = 0.6, π(ω=Q 2 ) = 0.4;

• Variable x, x correspond to the statuses of variable x of Q 3 from Fig. 7, before and after executing Q 3 ; the value of x is assumed and the value of x will be established by sampling S Q3 ;

x := 0; while x ≥ 0 do if prob(0.6) then if angel then

x := x + 1 else x := x -1 fi else if demon then x := x + 1 else x := x -1 fi fi od      Q 1      Q 2
Verbatim from [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF]: There is only one program variable x and no random variables. There is a while loop, where given a probabilistic choice, one of two statement blocks Q 1 or Q 2 is executed. The block Q 1 (resp., Q 2 ) is chosen to execute stochastically w.r.t. the probabilistic choice (Q 1 is selected with probability 0.6). The statement block Q 1 (resp., Q 2 ) is an angelic (resp., demonic) conditional statement to either increment or decrement x. Following [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF], call Q 3 the body of the while loop of this example: while x ≥ 0 do Q 3 . Figure 7: Semantics: SGS (Stochastic Game Structure) of Q 3 , Fig. 6 of [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF]. The execution begins with the probabilistic choice. The left branch (corresponding to Q 1 ) is selected according to demonic nondeterminism figured by a triangle, and the right branch (corresponding to Q 2 ) is selected according to angelic nondeterminism, figured by a diamond.

• It remains to define relation C involving ω, x, x . To mimic Fig. 7, we would like to write something like

x = if ω = Q 1 then angel x ∈ {x -1, x + 1} else demon x ∈ {x -1, x + 1}
Unfortunately, angelic/demonic choice are not concepts of our Mixed Systems model following Definition 1. With regard to probabilistic evaluation of state properties (item 3 of Definition 1), we could specify whether we use π (mirroring demonic) or π (mirroring angelic). Still, this does not allow to combine both alternatives for different parts of the system. We propose to refine Definition 1 so that both types of nondeterminism can be freely combined. Let us investigate this on the above example. Consider the Mixed System S = (Ω, π, X, C) ,

Inria where:

•

Ω = {Q 1 , Q 2 } and π(ω = Q 1 ) = 0.6, π(ω = Q 2 ) = 0.4;
• Variable x, x correspond to the statuses of variable x of Q 3 from Fig. 7, before and after executing Q 3 ; the value of x is assumed and the value of x will be established by sampling S Q3 ;

• Relation C is (yet informally) defined by

ωCx iff    ω = Q 1 ∧ angel x ∈ {x-1, x+1} or ω = Q 2 ∧ demon x ∈ {x-1, x+1} (46)
This definition for C is informal, since keywords demon and angel have no mathematical meaning by themselves. We will give a semantics to [START_REF] Loeliger | An introduction to factor graphs[END_REF] by assigning, to each state predicate, a probabilistic score π * . More precisely, we define π * (¬P ), the probabilistic score of predicate ¬P , by the following formula:

π * (¬P ) = def π c ({ω | ω=Q 1 ∧ ∃x ∈{x-1, x+1} : ¬P }) +π c ({ω | ω=Q 2 ∧ ∀x ∈{x-1, x+1} : ¬P }) (47)
In this formula, we give a semantics to angel in ( 46) by using the existential quantifier, i.e., we use the outer probability to evaluate the corresponding state predicate; we give a semantics to demon in ( 46) by using the universal quantifier, i.e., we use the inner probability to evaluate the corresponding state predicate. Now, for this example, π c = π since, with relation [START_REF] Loeliger | An introduction to factor graphs[END_REF], for both choices ω = Q 1 and ω = Q 2 , related values for state x exist. Formula (47) finally yields π * (¬P ) = 0.6.

The above coding applies only to a restricted class of relations C. In formula [START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF], we exploited the fact that, in relation C defined by [START_REF] Loeliger | An introduction to factor graphs[END_REF], a partition of Ω is performed first (probabilistic choice), and then, each branch of this choice involves a pure state predicate, independent from ω.

Here follow some hints to extend this link beyond the particular example. Our starting point is the semantics of Apps, which is expressed in terms of Stochastic Game Structures (SGS), see Definition 2.3 of [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF]. Since Mixed Systems do not support recursion, we consider only the subclass of SGS that are DAGs. Picking a probabilistic location of this SGS, we consider the maximal subgraph of this SGS that has as its only minimal location, and contains no other probabilistic location. For our example [START_REF] Lehmann | Testing statistical hypotheses[END_REF][START_REF] Loeliger | An introduction to factor graphs[END_REF][START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF], this yields the whole SGS. For each such subgraph, a coding similar to [START_REF] Lehmann | Testing statistical hypotheses[END_REF][START_REF] Loeliger | An introduction to factor graphs[END_REF][START_REF] Lunn | The BUGS project: Evolution, critique and future directions[END_REF] can be given. The partially ordered execution of the whole SGS is then mapped to a Bayesian network following Definition 9, and the incremental sampling of this Bayesian Network would correspond to the execution of the SGS as a game.

We preferred not to refine our Mixed System model with this additional feature, since, first, it applies only to a restricted class of relations C, and, second, we believe it to be incompatible with having a parallel composition.

A.2 Proof of Lemma 7

Proof: It is enough to prove the result for compressed systems. For i = 1, 2, let S i ≡ S i and let ϕ i be the bijections defining the two equivalences. We define ϕ(ω, q 1 q 2 ) = ((ω 1 , ω 2 ), q 1 q 2 ) where (ω i , q i ) = ϕ i (ω i , q i ), i = 1, 2

RR n°9447

and we have to verify that ϕ defines the desired equivalence between S = def S 1 S 2 and S = def S 1 S 2 . Using the fact that π = π 1 × π 2 , we get

C π = {(p 1 p 2 , ω, q 1 q 2 ) | q 1 q 2 ∧ ω 1 C 1 q 1 ∧ π 1 (ω 1 )>0 ∧ ω 2 C 2 q 2 ∧ π 2 (ω 2 )>0} = {(p, ω, q 1 q 2 ) | q 1 q 2 ∧ ω 1 C 1π q 1 ∧ ω 2 C 2π q 2 }
Thus, for every (p, ω, q 1 q 2 ) ∈ C π , we have q 1 = q 1 q 2 = q 2 and ω i C iπ q i , i = 1, 2, whence ω C π q and ϕ is a bijection. Since π = π 1 × π 2 we get π (ω ) = π(ω), which finishes the proof.

A.3 Proof of Theorem 13

Proof: We will repeatedly use notation [START_REF] Dempster | A generalization of bayesian inference[END_REF]. Without loss of generality we can assume that S is compressed. We first compress Margin Y (S) by considering the following equivalence relation, where Z = X \ Y and q Y , q Z are valuations for Y and Z:

ω ∼ Y ω iff ∀q Y :    ∃q Z : ωC(q Y , q Z ) ∃q Z : ω C(q Y , q Z )
; let ω Y be the equivalence class of ω.

Let C Y = def {(ω Y , q Y ) ∈ Ω Y × Q Y | ∃ω ∈ ω Y : ω Pr Y (C) q Y }
be the associated relation, and let π Y be the compressed probability defined by

π Y (ω Y ) = ω∈ω Y π(ω). Let us denote by S Y = (Ω Y , π Y , Y, C Y )
the resulting compressed system, and we recall that

Ω c Y = {ω Y | ∃q Y : ω Y C Y q Y }.
In the sequel, we feel free to identify ω Y ∈ Ω Y , an element of the set of equivalence classes, with ω Y seen as a subset of Ω saturated for ∼ Y . This way, a subset of Ω Y can also be interpreted as a subset of Ω.

To prove the theorem, we compare the two probabilistic semantics, namely: which state can be output and what is the outer probability of producing it. By definition of the sequential composition of kernels, Margin Y (S) ; Cond Y (S)

1. samples Margin Y (S) q Y ; and, then 2. given q Y , samples (Y =q Y ) S.

Regarding the relations governing the nondeterministic choice, the combination of these two steps is identical to C. Let q * be such that S q * , implying that Margin Y (S) q * Y , where q * Y = def Pr Y (q * ). Let us evaluate the outer probabilistic score of q * for the Bayesian network Margin Y (S) ; Cond Y (S), i.e., the probability that q * is a possible outcome of sampling Margin Y (S) ; Cond Y (S). We need to prove that it is equal to the probability that q * is a possible outcome of S, namely π c (C q * )-we used notation [START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF]. To show this, we note the following: 1. To output q * we first must output q * Y , which amounts to selecting ω Y such that ω Y C Y q * Y .

Using [START_REF] Baudart | Reactive probabilistic programming[END_REF], [START_REF] Chatterjee | Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs[END_REF] and notation [START_REF] Dahlqvist | Semantics of higher-order probabilistic programs with conditioning[END_REF], the probabilistic score of q * Y , i.e., the probability that q * Y is a possible outcome of Margin Y (S), is equal to

π c Y (C Y ) q * Y (48)
which is > 0 since Margin Y (S) q * Y .

Inria 2. Then, we must select ω using S, under the additional constraint that Pr Y (q) =q * Y , which requires that we sample ω ∈ Ω under the constraint that ω ∈ ω Y for some ω Y ∈ (C Y ) q * Y . The corresponding probabilistic score is thus equal to the conditional probability

π c C q * | (C Y ) q * Y , (49)
which is well defined since π c Y ((C Y ) q * Y ) > 0.

3. By [START_REF] Dempster | Upper and lower probabilities induced by a multivalued mapping[END_REF], the probabilistic score of q * is equal to the product of the two scores ( 48) and ( 49):

π c C q * | (C Y ) q * Y π c Y (C Y ) q * Y = π c C q * ∩ (C Y ) q * Y = π c C q *
, where the last equality follows from C q * ⊆ (C Y ) q * Y .

This shows that q * possesses identical probabilistic semantics, for the left and right hand side of Bayes formula.

A.4 Proof of Theorem 14

As a prerequisite, we need the following result: Lemma 23 Let S 1 and S 2 be any two Mixed Systems, and let Y be a set of variables containing X 1 ∩X 2 . Then, we have:

Margin X1∪Y (S 1 S 2 ) ≡ S 1 Margin Y (S 2 ).
Proof: This is immediate by observing that, first, Margin X1∪Y (S 1 S 2 ) on the one hand, and S 1 Margin Y (S 2 ) on the other hand, possess identical probability spaces, namely (Ω 1 , π 1 )×(Ω 2 , π 2 ), and, second, they possess identical relations Pr X1∪Y (C

1 ∧C 2 ) = C 1 ∧Pr X1∪Y (C 2 ) = C 1 ∧Pr Y (C 2 ).
The proof of Theorem 14 relies on the following lemma, which is a corollary of Bayes formula. This lemma provides the basic reasoning step of message passing algorithms:

Lemma 24 Let S 1 , S 2 , and Y be as in Lemma 23. Then:

S 1 S 2 ≡ P S 1 Margin Y (S 2 ) ; Cond Y (S 2 ) . (50)
Proof: For proving formula [START_REF] Mciver | Correctness by construction for probabilistic programs[END_REF], we first apply Theorem 13 with S replaced by S 1 S 2 , which yields:

S 1 S 2 ≡ P Margin X1∪Y (S 1 S 2 ) ; Cond Y (S 1 S 2 ).
Then, by Lemma 23, Margin X1∪Y (S 1 S 2 ) ≡ S 1 Margin Y (S 2 ) and then we conclude by observing that

S 1 Margin Y (S 2 ) ; Cond Y (S 1 S 2 ) ≡ P S 1 Margin Y (S 2 ) ; Cond Y (S 2 ) ,
since the outcome of S 1 is determined by the left hand factor of ";". Having proved this lemma, the proof of Theorem 14 reproduces exactly the reasoning steps establishing the message passing algorithm mapping factor graphs to Bayesian Networks in the classical setting [START_REF] Loeliger | An introduction to factor graphs[END_REF]; thus we only sketch here the argument of the proof. Proof: Since G S is a tree, a natural distance can be defined on the set of vertices of G S by taking the length of the unique path linking two vertices. Select an arbitrary system S o as an origin and partially order other systems according to their distance to the origin, let be this partial order. We have thus made G S a rooted tree, which we can see as a DAG. Then, the following two rules, known as message passing, are considered: R1: Pick S ∈ G S , let S ↑ be its (unique) ancestor in the tree and let X ↑ be the set of common variables of S ↑ and S. Then, let S < denote the parallel composition of all strict ancestors of S in G S and let X < be the set of variables of S < . Using Bayes formula, factor S as

S ≡ P Margin X ↑ (S) ; Cond X ↑ (S) ≡ P Margin X < (S) ; Cond X < (S) ,
where the second equivalence follows from the fact that additional variables belonging to X < \ X ↑ are not shared with S.

R2: Using formula (50) of Lemma 24, reorganize S by rewriting S < S ≡ P S < Margin X < (S) ; Cond X < (S) .

Rules R1 followed by R2 are successively applied starting from the leaves of the tree, down to its root. The result is a Bayesian Network.

B Proofs Regarding Mixed Automata

B.1 Proof of Lemma 18

Proof: The result is immediate if both S 1 and S 1 are compressed, see Definition 2. It is thus sufficient to prove the lemma for the following two particular cases: S 1 compresses to S 1 , and the converse. Consider first the case: S 1 compresses to S 1 . Let w(ω 1 , ω 2 ) be the weighting function associated to the lifting S 1 ρ S S 2 , and let π 1 (ω 1 ) = ω1∈ω 1 π 1 (ω 1 ) be the relation between π 1 and π 1 in the compression of S 1 to S 1 . Then w (ω 1 , ω 2 ) = ω1∈ω 1 w(ω 1 , ω 2 ) defines the weighting function associated to the lifting S 1 ρ S S 2 . The other properties required to deduce S 1 ρ S S 2 are immediate to prove. Now, consider the alternative case: S 1 compresses to S 1 , with relation

π 1 (ω 1 ) = ω 1 ∈ω1 π 1 (ω 1 ) (51)
between π 1 and π 1 , where ω 1 ∈ ω 1 means that ω 1 is the equivalence class of ω 1 with respect to relation ∼ defined in [START_REF] Benveniste | Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism[END_REF] when compressing S 1 . This case is slightly more involved since the weighting function w (ω 1 , ω 2 ) needs to be constructed. We need w (ω 1 , ω 2 ) to satisfy the following relations:

∀ω 1 : π 1 (ω 1 ) = ω2 w (ω 1 , ω 2 ) ∀ω 2 : π 2 (ω 2 ) = ω 1 w (ω 1 , ω 2 ) ∀(ω 1 , ω 2 ; q 1 ) : w (ω 1 , ω 2 ) > 0 ω 1 C 1 q 1 ⇒ ∃q 2 : ω 2 C 2 q 2 q 1 ρ q 2 . ( 52
)
Focus first on the first two lines of [START_REF] Pearl | Fusion, propagation, and structuring in belief networks[END_REF]. The following calculation shows that

w (ω 1 , ω 2 ) = def w(ω 1 , ω 2 ) × π 1 (ω 1 ) π 1 (ω 1 ) × 1(π 1 (ω 1 )>0) ,

Inria

where ω 1 is such that ω 1 ∈ ω 1 and 1(B) equals 1 if predicate B is true and 0 otherwise, yields a weighting function w satisfying the first two lines of (52):

ω2 w (ω 1 , ω 2 ) = ω2 w(ω 1 , ω 2 ) × π 1 (ω 1 ) π 1 (ω 1 ) × 1(π 1 (ω 1 )>0) = π 1 (ω 1 ) π 1 (ω 1 ) × 1(π 1 (ω 1 )>0) × ω2 w(ω 1 , ω 2 ) = π 1 (ω 1 ) ω 1 w (ω 1 , ω 2 ) = ω 1 w(ω 1 , ω 2 ) × π 1 (ω 1 ) π 1 (ω 1 ) × 1(π 1 (ω 1 )>0) = ω1 w(ω 1 , ω 2 ) × 1 π 1 (ω 1 ) × 1(π 1 (ω 1 )>0) ω 1 ∈ω1 π 1 (ω 1 ) =π1(ω1) = ω1 w(ω 1 , ω 2 ) = π 2 (ω 2 ) .
We move to the third line of ( 52). The conditions w (ω 1 , ω 2 ) > 0 and ω 1 C 1 q 1 together imply w(ω 1 , ω 2 ) > 0 and ω 1 C 1 q 1 where ω 1 is the equivalence class of ω 1 , i.e., ω 1 ∈ ω 1 . The right hand side then follows since we have S 1 ρ S S 2 . This finishes the proof.

B.2 Proof of Lemma 20

Proof:

Set M = def M 1 M 2 and M = def M 1 M 2 .
Define the relation ≤ between Q and Q by: q ≤ q iff q 1 ≤ 1 q 1 and q 2 ≤ 2 q 2 . Let us prove that ≤ is a simulation. Let q be such that q α -→ M S for some consistent S . Then, q = q 1 q 2 and S = S 1 S 2 . By definition of the parallel composition, we have q i αi -→ M i S i for i = 1, 2, with α 1 Σ α 2 and α = α 1 Σ α 2 . Since q i ≤ q i , we derive the existence (and uniqueness) of consistent systems S i , i = 1, 2 such that q i αi -→ Mi S i . Since q = q 1 q 2 we have q 1 q 2 and, thus, by definition of the parallel composition, we deduce r α -→ M S 1 S 2 . It remains to show that S 1 S 2 is consistent. To prove this, remember that S = S 1 S 2 is consistent. Thus, there exist compatible q 1 and q 2 such that S i q i , i = 1, 2. By definition of the simulations ≤ i , we deduce that S i q i , i = 1, 2, which shows that S 1 S 2 is consistent. Proof: The sampling of spa P is: if P is in state q∈Q, performing α∈Σ leads to some target set of probability distributions over Q, of which one is selected, nondeterministically, and used to draw at random the next state q . We can reinterpret this sampling as follows: performing α∈Σ while being in state q∈Q leads to the same target set of probability distributions over Q, that we use differently. We form the direct product of all distributions belonging to the target set and we perform one trial according to this distribution, i.e., we perform independent random trials for all probabilities belonging to the target set. This yields a tuple of candidate values for the next state, of which we select one, nondeterministically.

C Proofs Regarding the comparison with Probabilistic Automata

Clearly, these two samplings produce identical outcomes. The latter is the sampling of Mixed Automaton

M P = (Σ, {ξ}, q 0 , → P ) , (53)
defined as follows:

1. Alphabet Σ of M P is identical to that of P ;

2. The unique variable ξ of M P enumerates the values of Q, and initial state q 0 is identical to that of P ; hence, P and M P possess identical sets of states, related via the identity map;

3. → P maps a pair (q, α) ∈ Q×Σ to the mixed system S(q) = (Ω, Π, ξ, q, C), where:

(a) Ω is the product of n copies of Q, where n is the cardinality of the set {π | (q, α, π)∈ → }; thus, ω is an n-tuple of states: ω=(q 1 , . . . , q n ). (b) Π is the product of all probabilities belonging to {π | (q, α, π)∈ →}; (c) Relation C is defined by (ω, q ) ∈ C if and only if q ∈ {q 1 , . . . , q n }. So, we map spa P to Mixed Automaton M P , defined in [START_REF] Pearl | Causality[END_REF].

Mapping simulation relations: Defining simulation relations for pa requires lifting relations, from states to distributions over states. The formal definition for this lifting, as given in Section 4.1 of [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF], corresponds to our Definition 17, when restricted to purely probabilistic mixed systems. The same holds for the strong simulation relation defined in Section 4.2 of the same reference: it is verbatim our Definition 19, when restricted to purely probabilistic mixed systems. This proves the part of Theorem 21 regarding simulation.

Mapping parallel composition:

We move to parallel composition, for which the reader is referred to [START_REF] Lynch | Compositionality for probabilistic automata[END_REF], Section 3. For P 1 = (Σ, Q 1 , q 0,1 , → 1 ) and P 2 = (Σ, Q 2 , q 0,2 , → 2 ) two PA, their parallel composition is P = P 1 P 2 = (Σ, Q 1 × Q 2 , (q 0,1 , q 0,2 ), →), where

(q 1 , q 2 ) α -→ π 1 ×π 2 iff q i α -→ i π i for i = 1, 2 (54)
So, on one hand we consider the Mixed Automaton M P . On the other hand, we consider the parallel composition of their images M P1 and M P2 , namely M = M P1 M P2 = (Σ, {ξ 1 , ξ 2 }, (q 0,1 , q 0,2 ), → 12

). In M , the state space is the domain of the pair (ξ 1 , ξ 2 ), namely Q 1 × Q 2 , and, since there is no shared variable between the two Mixed Automata, the transition relation → 12 is given by:

(q 1 , q 2 ) α -→ 12 S 1 S 2 iff q i α -→ i S i for i = 1, 2 (55)
We thus need to show that M P and M are simulation equivalent.

We will actually show that the identity relation between the two state spaces (both are equal to

Q 1 × Q 2 ) is a simulation relation in both directions.
Observe first that ( 54) and ( 55) differ in that the former involves a nondeterministic transition relation, whereas the latter involves a deterministic transition function, mapping states to mixed systems. Pick (q 1 , q 2 ) ∈ Q 1 × Q 2 and consider a transition for M P :

(q 1 , q 2 ) α -→ M P S = ((Ω, Π), ξ, (q 1 , q 2 ), C) where we have, for S:

Inria

• Ω is the product of n 1 copies of Q 1 and n 2 copies of Q 2 , where, for i = 1, 2, n i is the cardinality of the set {π i | (q i , α, π i ) ∈→ i }, so that ω identifies n 1 × n 2 -tuple of states: ω = (q 11 , . . . , q 1n1 ; q 21 , . . . , q 2n2 );

• Π is the product of all probabilities belonging to set {π 1 × π 2 | (q i , α, π i ) ∈→ i };

• ξ has domain Q 1 × Q 2 ;

• (ω, (q 1 , q 2 )) ∈ C if and only if

(q 1 , q 2 ) ∈ {(q 1i1 , q 2i2 ) | i 1 ∈ {1, . . . , n 1 } and i 2 ∈ {1, . . . , n 2 }} .
Next, pick (q 1 , q 2 ) ∈ Q 1 × Q 2 and consider a transition for M , see [START_REF] Martin L Puterman | Markov decision processes: discrete stochastic dynamic programming[END_REF]. We need to detail what S 1 S 2 = ((Ω , Π ), ξ , (q 1 , q 2 ), C ) is. We have, for S 1 S 2 :

• Ω is still the product of n 1 copies of Q 1 and n 2 copies of Q 2 ;

• Π is the product Π 1 × Π 2 , where Π i is the product of all probabilities belonging to set

{π i | (q i , α, π i ) ∈ → i }; • ξ has domain Q 1 × Q 2 ;
• (ω, (q 1 , q 2 )) ∈ C if and only if 1. The alphabet Σ of P M is identical to that of M ;

(q 1 , q 2 ) ∈ {(q 1i1 , q 2i2 ) | i 1 ∈ {1, . . . ,
2. The set of states Q of P M is equal to the set of states of M , namely the domain of its set X of variables;

3. For S = (Ω, π, X, p, C), decompose relation {(ω, q)|ωCq} as ψ∈Ψ C graph(ψ), where Ψ C denotes the set of all partial functions Ω → Q, mapping each ω ∈ ∃q.C to some q such that ωCq. Then, we consider, for each ψ ∈ Ψ C , the measure defined by ψ[π](q) = def π(ψ -1 (q)), where ψ -1 (q) = {ω|ψ(ω)=q} (ψ[π] is the image of π by ψ), and we renormalize it by considering

ψ[π] ψ[π](Q) ,
thus obtaining a probability distribution over Q. This defines a subset P S ⊆ P(Q) of probability distributions.

4. The transition relation of P M is defined as follows:

→ P M = {(p, α, µ) | ∃S : (p, α, S) ∈ → M and µ ∈ P S } (57)
System S 1 amounts to defining the pair (x 1 , x) as random variables with joint distribution π 1 ; similarly, S 2 amounts to defining the pair (x, x 2 ) as random variables with joint distribution π 2 . We assume that the set of all q∈Q x such that π 1 (Q 1 ×{q})>0 and π 2 ({q}×Q 2 )>0 is non empty. Forming the composition S 1 S 2 yields the system S(p)=(Ω, π, X, p, C), where X = X 1 ∪X 2 = {x 1 , x, x 2 }, Q = Q x1 ×Q x ×Q x2 , p = p 1 p 2 , Ω = Ω 1 × Ω 2 , π = π 1 × π 2 , and ωC(q 1 , q, q 2 ) iff ω 1 C 1 (q 1 , q) and ω 2 C 2 (q, q 2 ). According to Definition 1, the sampling of S is the following: draw (ω 1 , ω 2 ) at random with the conditional distribution π 1 × π 2 (ω 1 , ω 2 )|x(ω 1 )=x(ω 2 ) , where the map x was defined in [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]; the resulting (ω 1 , ω 2 ) uniquely defines (q 1 , q, q 2 ) ∈ Q (no nondeterminism). In words, the parallel composition S 1 S 2 amounts to making the triple of variables (x 1 , x, x 2 ) to be random with the joint distribution π 1 × π 2 (ω 1 , ω 2 ) | x(ω 1 ) = x(ω 2 ) . Next, consider the Mixed Automaton M =({α}, X, q 0 , →), where X={x 1 , x, x 2 }, set Q of states is defined accordingly Q=Q x1 ×Q x ×Q x2 , and → maps, through action α, any state p∈Q to the above system S(p). Similarly, we consider the two Mixed Automata M i = ({α}, X i , q i,0 , → i ), i=1, 2, where X i is as above, q i,0 is the projection of q 0 on Q i , and → i maps, through action α, any state p i ∈Q i to the above system S i (p i ). We have M = M 1 M 2 .

The only candidate way of mapping M i to a spa is by considering the two spa P i with sets of states Q i and transition relation p i α -→ i π i , where π i was defined above. Now, P 1 P 2 has transition relation p α -→ π 1 × π 2 , which reflects no interaction between the two spa, so it cannot represent M 1 M 2 .

C.2 Proof of Theorem 22 regarding Probabilistic Automata

Proof: We consider the mapping P → M P = ({1}, X, q 0 , → M P ), from pa to Mixed Automata, defined as follows:

1. Alphabet {1} is the trivial singleton (the particular element does not matter); 2. X = {ξ Σ , ξ Q }, where the variables ξ Σ and ξ Q enumerate Σ and Q; 3. Transition → M P maps state p to system S(p) = ((Ω, π), X, p, C), where

• Ω = (Σ×Q) n , where n is the cardinal of the image of p by transition →;

• π is the product of all the distributions selected by transition → starting from p;

• C is the nondeterministic selection of one component of ω.

We only need to prove the positive statement related to simulation. Consider a simulation relation for pa q ≤ q . We need to prove that ≤ is also a simulation relation for Mixed Automata. Let µ be such that (q, µ) ∈ →. Since ≤ is a simulation relation for pa, there exists µ such that (q , µ ) ∈ → and µ ≤ P µ . Let S and S be the mixed systems to which q and q are mapped by step 3 of the mapping P → M P . We have to prove that S ≤ S S . For each µ such that (q, µ) ∈ →, let the function χ : P(Q) → P(Q ) select one µ such that (q , µ ) ∈ → and µ ≤ P µ and let v µ be a weighting function associated to relation µ ≤ P µ . The following weighting function w(ω, ω ) = def µ:(q,µ)∈ → v µ (q µ , q µ ) where (q µ , q µ ) ∈ Q×Q , solves the problem.

D Extending Mixed Systems to continuous probabilities

In this appendix, we indicate how to relax the restriction that the considered probability spaces should all be discrete and we discuss technical difficulties. A recommended reference on probability theory is [START_REF] Dellacherie | Probabilities and potentials[END_REF]. The reader is invited to compare the following writing with the corresponding material of Section 2. We begin with some notations and prerequisites.

D.1 Notations and prerequisites on probability theory

For P and Q two sets, P × Q their product, and A ⊆ P × Q, we denote by Pr P (A) the projection of A over P .

Probability spaces: (Ω, F, π) shall generically denote a probability space, i.e., Ω is a set, F is a σ-algebra over Ω (i.e., a subset of 2 Ω , containing ∅ and stable under complement, and countable unions and intersections), and π is a probability (i.e., a countably additive function, from σalgebra F to [0, 1], such that π(∅) = 0 and π(Ω) = 1). Let p : (Ω, F) → {0, 1} be a measurable predicate, say that p holds almost everywhere if π{ω | p(ω) = 1} = 1. For a measurable function f : (Ω, F) → (R + , L), where L is the Borel σ-algebra over R + , we write

E(f ) = def f (ω)π(dω) .
For (Ω i , F i , π i ) i=1,2 two probability spaces, F 1 × F 2 is defined as the smallest σ-algebra over Ω 1 × Ω 2 making the two projections measurable, and π 1 × π 2 shall denote the cartesian product of the two probabilities, characterized by (π 1 × π 2 )(A 1 × A 2 ) = π 1 (A 1 )π 2 (A 2 ), where A i ∈ F i . Infinite products of probabilities π = i∈I π i with arbitrary index set I can even be defined; they are characterized by the equalities π i∈I A i = i∈I π i (A i ), where all but a finite number of A i are equal to Ω i .

Conditional expectations and conditional probabilities:

For A ∈ F, let 1 A denote the characteristic function of set A, which equals 1 on A and 0 elsewhere; then, we write with a similar result for 1 Ω-B , showing that the characterization of the conditional expectation is satisfied. This establishes the link between conditional expectation and conditional probability in its elementary setting.

π(A | G) = def E(1 A | G). (60

Inria

For this case, the correction is easily guessed. The aim is that prior probability π should be replaced by the posterior conditional distribution π(• | y), rather a disintegration for it. This amounts to making y "variable" by considering a disintegration π(A | F Y ) according to Definition 26, where F Y ⊂ F is the σ-algebra generated by random variable Y . Recall that the existence of such a disintegration is subject to topological conditions, see the comment following Definition 26-such conditions are satisfied by this example. Then, we take π c = π(• | y) by taking the corresponding disintegration.

How can we extend this to general Mixed Systems? Informally, how can we make relation C "variable"? Definition 29 (consistency and sampling) Mixed System S is called consistent if the following conditions hold:

The sampling of S consists in: (1) drawing ω at random using π c , and (2) nondeterministically selecting q such that ωCq. This two-step procedure is denoted by S q.

The "variable embedding" of C is the relation C, from which C is retrieved by selecting the atom w at step 2a.

Example 10 Consider the ReactiveBayes program "S 1 S 2 S 3 S 4 " of the introduction. Now, the white noise model for w in Noise is truly Gaussian (or any other distribution on R, possibly continuous). The prior probability of this system is prior proba :    rf n ∼ Bernoulli(10 -6 ) v n ∼ µ by semantic convention, rf and w are independent [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF] and relation C is the following system of equations:

C :            observe u, y x 0 = c x , v 0 = c v , f 0 = F x n = ϕ(u n , x n-1 )
y n = if f n then ψ(x n , v n ) else x n f n = (rf n or f n-1 ) and not bk n [START_REF] Wang | A denotational semantics for low-level probabilistic programs with nondeterminism[END_REF] The following observation is the key to handle the model [START_REF] Van De Meent | An introduction to probabilistic programming[END_REF][START_REF] Wang | A denotational semantics for low-level probabilistic programs with nondeterminism[END_REF]: if we forget for a while the first constraint observe y in (66), then the resulting dynamical system can be seen as an input/output system with inputs u, v, rf , of which u is a measured input, whereas v, rf are random inputs: there is nothing unusual. In this i/o system, the prior probability is not subject to any constraint, hence the posterior probability equals the prior.

The difficulty comes with the consideration of the output constraint observe y. This suggests taking for the instrumental σ-algebra H the σ-algebra generated by y. Accordingly, we partition (66) as where f is the function resulting from computing y from the pair (w, rf ) by using system of equations [START_REF] Wang | A denotational semantics for low-level probabilistic programs with nondeterminism[END_REF] in which the first equation has been deleted (other variables are also computed). This defines the auxiliary relation C and we have Ω c = Ω. The σ-algebra F is generated by the pair (w, rf ) of random variables, and H is the σ-algebra generated by y = def f (w, rf ). Atoms of H consist of any reachable value for y. Then, π(• | H) = π(• | y) is the conditional distribution of the pair (w, rf ) given a reachable value for y, and Ω c = Ω, showing that the considered system is consistent.

As a side result, the discussion of this example suggests how sampling can be performed in practice for ReactiveBayes programs involving continuous distributions.

Inria

RESEARCH CENTRE RENNES -BRETAGNE ATLANTIQUE

Figure 1 :

 1 Figure 1: Intuitive picturing of a Mixed System having two variables x and y.

Figure 2 :

 2 Figure 2: The marginal on y for the Mixed System of Figure 1 is by hiding x (in red).

Definition 5 (

 5 marginal) Let S = (Ω, π, X, C) be a Mixed System, and let Y ⊆ X be a subset of variables. The marginal of S on Y , denoted by Margin Y (S), is the Mixed System Margin Y (S) = def (Ω, π, Y, Pr Y (C)).

Figure 5 :

 5 Figure 5: Illustrating the right hand side of Bayes' formula: the output Y of the system on the left is connected to the input Y of the kernel on the right.

Example 1

 1 Mixed System S 1 , specified by model (1) writes observe u init x = x0 y = phi(u,pre x) x = if fail then psi(y,noise) else y Mixed System S 2 , specified by model (2) writes init noise = n0 noise = chi(pre noise,w) w ∼ mu And so on. The global model is S 1 S 2 S 3 S 4 .

α

  ::= • e, where e has Boolean type A ::= on α then S else S | A A

Figure 6 :

 6 Figure 6: Example of Fig. 2 of [21]

C. 1

 1 Proof of Theorem 21 regarding Simple Probabilistic Automata C.1.1 Statement 1 of Theorem 21: from SPA to Mixed Automata

  For G ⊆ F a sub-σ-algebra of F, and X : (Ω, F) → R + , measurable, there exists Y : (Ω, G) → R + , measurable, such that E(X×Z) = E(Y ×Z) for any measurable Z : (Ω, G) → R + . Y satisfying the above properties is almost surely unique: π(Y = Y ) = 0 for any two such random variables. Y is called the conditional expectation of X given G, written E(X | G).

  ) If B ∈ F satisfies π(B) > 0 and F B = {∅, Ω, B, Ω\B} is the smallest σ-algebra containing set B, then, the conditional expectation f = def π(A | F B ) is such that f (ω) = π(A | B) = π(A∩B)π(B) for almost every ω ∈ B. To show this, we formE(π(A | G) × 1 B ) = E π(A∩B) π(B) × 1 B = π(A∩B) π(B) × E (1 B ) =π(B)= π(A∩B)

1 .

 1 There exists a sub-σ-algebra H ⊆ F such that a disintegration π(• | H) exists; we denote by a a generic atom of H, thus conditional probability π(• | H) becomes a function of atom a, so we write it π(• | a); 2. There exists a measurable relation C ∈ F × G such that (a) Relation C takes the form C = C ∩ (a × Q) for some atom a of H; (b) π(Ω c | a) > 0 where Ω c = def {ω | ∃q : ωCq}. If S is consistent, define π c by π c (A) = def π(A ∩ Ω c | a) π(Ω c | a)

  the σ-algebra generated by y, whose atom is represented by a value for y.y n = f (v n , rf n )defining C and consistency set Ω c , equal to Ω (67)

  whereas M P1 P2 and M P1 M P2 are simulation equivalent. See Appendix C.2 for a proof. Due to Statement 2 of Theorem 21 and the existence of an embedding spa→pa [60] preserving simulation, a reverse mapping exists, from Mixed Automata to pa.

2. There exists a reverse mapping M →P M , from Mixed Automata to spa, preserving simulation. No reverse mapping exists, however, that preserves parallel composition.

See Appendices C.1.1 and C.1.2 for proofs of Statements 1 and 2 of this theorem. The two mappings P →M P and M →P M are not opposite, which makes it possible for the two statements not to contradict each other. The non-existence of a reverse mapping M →P M preserving parallel composition highlights that the difference in the parallel compositions, for SPAs vs. for Mixed Automata, is deep.

Theorem 22 (PA vs. Mixed Automata) There exists a mapping P →M P , from pa to Mixed Automata, preserving simulation. Parallel composition, however, is not preserved.

RR n°9447

Outer and inner probabilities were called upper and lower in[START_REF] Dempster | Upper and lower probabilities induced by a multivalued mapping[END_REF].Inria

This theorem and formula[START_REF] Benveniste | The synchronous languages 12 years later[END_REF] correct the erroneous construction of the conditional Cond Y (S) in Appendix A of[START_REF] Benveniste | A calculus of stochastic systems for the specification, simulation, and hidden state estimation of mixed stochastic/nonstochastic systems[END_REF].RR n°9447

Inria

Depending on the authors, disintegration is also called regular version of the conditional expectation.RR n°9447

They are actually called "Lusin spaces" in[START_REF] Blackwell | On a class of probability spaces[END_REF], but the term "Backwell spaces" has been used since then in the literature to avoid the confusion with the hierarchy of Polish topological spaces.Inria

Acknowledgements: The reviewers are gratefully thanked for pointing weaknesses and suggesting important bibliographical items while commenting the original version.

Consider two Mixed Automata M, M and let ≤ be a simulation relation between their state spaces Q and Q : q ≤ q and q α -→ M S imply the existence of S ∈ S(Q ) such that S ≤ S S and q α -→ M S . We need to show that the same relation ≤ ⊆ Q×Q is also a simulation relation for spa. Let q α -→ P M µ be a transition of spa P M . By [START_REF] Segala | Probability and nondeterminism in operational models of concurrency[END_REF], there exists a Mixed System S such that q α -→ M S and µ ∈ P S . Since ≤ is a simulation relation for Mixed Automata, there exists S ∈ S(Q ) such that S ≤ S S and q α -→ M S . Now, S ≤ S S expands as follows: There exists a weighting function w : Ω × Ω → [0, 1] such that the following two conditions hold:

1. For every triple (ω, ω ; q) such that w(ω, ω ) > 0 and ωCq, there exists q such that ω C q and q ≤ q ;

2. w projects to π and π , respectively.

Let ψ ∈ Ψ C be the selection function giving rise to µ following step 3, meaning that µ is obtained by renormalizing ψ[π]. Select any ω ∈ ∃q.C and let q = ψ(ω). Select any ω such that w(ω, ω ) > 0 and assign to it one q such that ω C q and q ≤ q (such an q exists by the above Condition 1). This selection procedure defines a selection function ψ : ∃q C → Q , mapping the ω of the above Condition 1 to q , which in turn defines a probability distribution µ , obtained by renormalizing ψ [π ]. Consider the following weighting function over Q×Q : v = (ψ, ψ ).w , which expands as

In particular v(q, q ) ≥ w(ω, ω ) > 0 by construction of ψ, ψ , and v. Then, v projects to µ, and to µ :

and ∀q :

To summarize, we have constructed a probability distribution µ such that µ ≤ P µ and q α -→ P M µ , showing that ≤ was also a simulation relation for spa. To complete our proof, it remains to show the following lemma:

Lemma 25 There is no mapping M → P M that preserves the parallel composition.

To support the above claim, we consider the following counter-example, where S(p) indicates that S has previous state p:

Inria

For G 2 , G 1 ⊆ F two sub-σ-algebras, and

. Let B ∈ F and G ⊆ F, and let F B be the smallest σ-algebra containing the set B; we write

Disintegration: Consider (Ω, F, π) and G ⊆ F as before. So far we have defined π(A | G) as a G-measurable random variable, for a given A ∈ F. Can we take it as a transition probability P (ω, A), i.e., a map such that A → P (ω, A) is a probability for ω fixed, and ω → P (ω, A) is G-measurable for A fixed? Here is the formalization: Existence of a disintegration: The existence of a disintegration is not always guaranteed. It is obvious for discrete probability spaces. It is not true in general, however, see, e.g., [START_REF] Blackwell | On a class of probability spaces[END_REF]. Failure to exist typically occurs when working with measurable spaces completed with subsets of zero probability sets. The existence of a a disintegration is only guaranteed under specific topological properties for the underlying set. Jirina Theorem is an example of broad sufficient topological conditions for the existence of regular versions for conditional expectations, see [START_REF] Dellacherie | Probabilities and potentials[END_REF][START_REF] Halmos | Measure Theory. Graduate Texts in Mathematics[END_REF]. The Blackwell spaces, however, are adequate tools for this, so we introduce them next. For the following material, the reader is referred to [START_REF] Blackwell | On a class of probability spaces[END_REF].

If Ω is a metric space, the smallest σ-algebra containing all open sets of Ω is its Borel σalgebra, denoted by B. Borel σ-algebra B is called separable if there is a sequence B n ∈B such that B is the smallest Borel σ-algebra containing all B n . In particular, if Ω is a separable metric space, its Borel σ-algebra is separable. The atoms of B are the sets B ∈ B such that no proper nonempty subset of it belongs to B. Any two nonidentical atoms are disjoint and every Borel set is a union of atoms.

A metric space A will be called analytic if A is the continuous image of the set of irrational numbers. The following properties hold, showing which cases are covered by this notion:

D.2 Definition and basic properties

Relations: Upper case letters X, Y, Z shall denote finite sets of variables, and variables are denoted by corresponding lower case letters x, y, z . . . Let the domain of x be denoted by Q x and be equipped with a σ-algebra G x ; the domain of X is Q X = def x∈X Q x , equipped with the product σ-algebra G X = x∈X G x . We will consider equations (also called relations or constraints): an equation on X identifies with its set of solutions, i.e., a measurable subset of Q X ; if Y ⊆ X, an equation on Y can be seen as an equation on X. We consider systems of equations, which are sets of equations implicitly composed via intersection.

Definition 28 (Mixed System) A Mixed System is a tuple

where (Ω, F, π) is a private probability space; (Q x , G x ) x∈X is a finite set of measurable state spaces with product (Q, G) = def x∈X (Q x , G x ), and C ∈ F×G is a measurable relation over Ω×Q. In the sequel, we also write ωCq to mean (ω, q) ∈ C, and we identify the set of variables X with the measurable state space (Q x , G x ) x∈X it defines, thus we write

for short instead of (62).

Defining the semantics of Mixed Systems in the general case requires some care, as the following example shows.

Example 9 [discussing consistency] Let X and Y be two real random variables with continuous joint distribution π. Formally, Ω = R 2 , F is the Lebesgue σ-algebra over Ω, π is a continuous probability over (Ω, F) and X and Y are the first and second coordinates of R 2 . For y a given value for Y , consider C = {(ω, y) | ω ∈ Ω} completing the definition of Mixed System S = (Ω, F, π), X, C . The intuition is that S models the conditional distribution of (X, Y ) given that Y = y. We would like this to be a consistent system, despite π(Y =y) = 0. Thus, elementary Definition 1 for the operational semantics cannot be used since it would lead to considering system S as inconsistent.