SOS-BASED MODAL DECOMPOSITION ON NONDETERMINISTIC PROBABILISTIC PROCESSES 7 VALENTINACASTIGLIONI,DANIELGEBLER, ANDSIMONETINI 1 0 University of Insubria, Como, Italy 2 e-mail address: [email protected] n VU University,Amsterdam, The Netherlands a e-mail address: [email protected] J 8 University of Insubria, Como, Italy 2 e-mail address: [email protected] ] O Abstract. We propose a method for the decomposition of modal formulae on processes L with nondeterminism and probability with respect to Structural Operational Semantics. . The purpose is to reduce the satisfaction problem of a formula for a process to verifying s c whetheritssubprocessessatisfycertainformulaeobtainedfromthedecomposition. Todeal [ with theprobabilistic behaviorof processes, and thuswith thedecomposition of formulae characterizing it, we introduce a SOS-like machinery allowing for the specification of the 1 behavior of open distribution terms. By our decomposition, we obtain (pre)congruence v formats for probabilistic bisimilarity, ready similarity and similarity. 0 3 3 8 0 1. Introduction . 1 Behavioral equivalences and modal logics have been successfully employed for the specifi- 0 7 cation and verification of communicating concurrent systems, henceforth processes. The 1 former ones, in particular the family of bisimulations, provide a simple and elegant tool : v for the comparison of the observable behavior of processes. The latter ones allow for an i immediate expression of the desired properties of processes. Since the work of [HM85] on X the Hennessy-Milner logic (HML), these two approaches are connected by means of logical r a characterizations of behavioral equivalences: two processes are behaviorally equivalent if and only if they satisfy the same formulae in the logic. Hence, the characterization of an equivalence subsumes both the fact that the logic is as expressive as the equivalence and the fact that the equivalence preserves the logical properties of processes. However, the connection between behavioral equivalences and modal logics goes even further: modal decomposition of formulae exploits the characterization of an equivalence 1998 ACM Subject Classification: F.3.2. Key words and phrases: SOS, nondeterministic probabilistic process algebras, logical characterization, decomposition of modal formulae. A preliminary version of this paper appeared as [CGT16b]. LOGICALMETHODS (cid:13)c ValentinaCastiglioni,DanielGebler,andSimoneTini INCOMPUTERSCIENCE DOI:10.2168/LMCS-??? CreativeCommons 1 2 VALENTINACASTIGLIONI, DANIELGEBLER,ANDSIMONETINI to derive its compositional properties. Roughly speaking, the definition of the seman- tic behavior of processes by means of the Structural Operational Semantics (SOS) frame- work [Plo81] allowed for decomposing the satisfaction problem of a formula for a process into the verification of the satisfaction problem of certain formulae for its subprocesses (see [BFvG04, FvG16, FvGdW06, FvGdW12, LX91]) by means of the notion of ruloid [BIM95], namely inference transition rules that are derived from the SOS specification and define the behavior of open processes in terms of the behavior of their variables. Then, in [BFvG04, FvG16, FvGdW12], the decomposition of modal formulae is used to sys- tematically derive expressive congruence (precongruence) formats for several behavioral equivalences (preorders) from their modal characterizations. Further, in [GF12] the seman- tic model of reactive probabilistic labeled transition systems [vGSS95] is considered and a methodfordecomposingformulaefromaprobabilisticversionofHML[PS07]characterizing probabilistic bisimilarity wrt. a probabilistic transition system specification in the format of [LT09] is proposed. Our purpose is to extend the SOS-driven decomposition approach to processes in which the nondeterministic behavior coexists with probability. To this aim we take the very general semantic model of nondeterministic probabilistic transition systems (PTSs) of [DL12, Seg95b]. In the PTS model, processes perform actions and evolve to probability a distributions over processes, i.e. an a-labeled transition is of the form t −→ π, with t a pro- cess and π a distribution holding all information on the probabilistic behavior arising from this transition. All modal logics developed for the PTS model are equipped with modal- ities allowing for the specification of the quantitative properties of processes. In essence, this means that some modal formulae are (possibly indirectly) evaluated on distributions. In order to decompose this kind of formulae, we introduce a SOS-like machinery, called distribution specification, in which we syntactically represent open distribution terms as probability distributions over open terms. More precisely, our distribution specification, consisting in a set of distribution rules defined on a signature, will allow us to infer the q expression Θ −→ t whenever a closed distribution term Θ assigns probability weight q to a closed term t. Then, from these distribution rules we derive the distribution ruloids, which willplayafundamentalroˆleinthedecomposition method. Infact, ashappensforruloidson q terms, our distribution ruloids will allow us to derive expressions of the form Θ −→ t, for an arbitrary opendistributionterm Θandopenterm t, by consideringonly thebehavior of the variables occurringinΘ. Hence, theywillallow ustodecomposetheformulaecapturingthe quantitative behaviorofprocessessincethroughthemwecanrelatethesatisfaction problem of a formula of this kind for a closed distribution term to the satisfaction problem of cer- tain derived formulae for its subterms. We stress that our distribution ruloids can support the decomposition of formulae in any modal logic for PTSs and moreover the distribution specification we have developed can be easily generalized to cover the case of models using sub-distributions in place of probability distributions (see for instance [LdV15, LdV16]). We present the decomposition of formulae from the two-sorted boolean-valued modal logic L of [DD11]. This is an expressive logic, which characterizes probabilistic bisimilarity [DD11] and bisimilarity metric [CGT16a]. We apply our decomposition method also to two subclasses of formulae in L, denoted by L and L , which we prove to characterize, respec- r + tively, probabilistic ready similarity and similarity. Finally, to show the robustness of our approach we apply it to derive the congruence theorem for probabilistic bisimilarity wrt. SOS-BASED MODAL DECOMPOSITION ON NONDETERMINISTIC PROBABILISTIC PROCESSES 3 the PGSOS format [DGL14] and the precongruence theorem for probabilistic ready simi- larity and similarity wrt. the PGSOS format and the positive PGSOS format, respectively. Summarizing: (1) We present new logical characterizations of probabilistic ready similarity and simi- larity obtained by means of two sublogics of L, resp. L and L (Theorem 2). r + (2) We define a SOS machinery for the specification of the probabilistic behavior of processes, which can support the decomposition of any modal logic for PTSs. (3) We develop a method of decomposing formulae in L and in its sublogics L and L r + (Theorem 6 and Theorem 7). (4) We derive (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity by exploiting our decomposition method on the logics characterizing them (Theorem 8). The paper is organized as follows: in Section 2 we recall some base notions on the PTS model, the PGSOS specification, probabilistic (bi)simulations and their logical char- acterizations. In particular we provide the characterization results for probabilistic ready similarity and similarity. In Section 3 we introduce the SOS-like machinery for the spec- ification of the behavior of distribution terms and in Section 4 we define the two classes of ruloids: the P-ruloids, built on a PGSOS specification P, and the distribution ruloids, derived from a distribution specification. Section 5 is the core of our paper and provides our decomposition method and the derivation of the (pre)congruence formats for proba- bilistic bisimilarity, ready similarity and similarity. Finally we end with some conclusion and discussion of future work in Section 6. 2. Probabilistic Transition Systems 2.1. The PTS model. A signature is given by a countable set Σ of operators. We let f range over Σ and n range over the rank of f. We assume a countable set of (state) variables V disjoint from Σ. For a set of variables V ⊆ V , the set T(Σ,V) of terms s s over Σ and V is defined as the least set such that: (i) x ∈ T(Σ,V) for all x ∈ V, and (ii) f(t ,...,t ) ∈ T(Σ,V) whenever f ∈ Σ and t ,...,t ∈ T(Σ,V). By T(Σ) we denote 1 n 1 n the set of the closed terms T(Σ,∅). By T(Σ) we denote the set of the open terms T(Σ,V ). s Nondeterministic probabilistic transition systems (PTSs) [DL12, Seg95b] extend LTSs by allowing for probabilistic choices in the transitions. The state space is the set of the a closed terms T(Σ). The transitions are of the form t −→ π, with t a term in T(Σ), a an action label and π a probability distribution over T(Σ), i.e. a mapping π: T(Σ) → [0,1] with π(t) = 1. By ∆(T(Σ)) we denote the set of all probability distributions over t∈T(Σ) T(Σ). P Definition 1 (PTS, [DL12, Seg95b]). A Nondeterministic Probabilistic Labeled Transition System (PTS) isatripleP = (T(Σ),A,−→), where: (i)Σis asignature, (ii)Ais acountable set of actions, and (iii) −→⊆ T(Σ)×A×∆(T(Σ)) is a transition relation. We say that a PTS P = (T(Σ),A,−→) is image finite if each closed term in T(Σ) has finitely many outgoing a-labeled transitions for each a ∈ A. For a distribution π ∈ ∆(T(Σ)), we denote by supp(π) the support of π, namely supp(π) = {t ∈ T(Σ) | π(t) > 0}. For a term t ∈ T(Σ), we denote by δ the Dirac t distribution such that δ (t) = 1 and δ (s) = 0 for s 6= t. For f ∈ Σ and π ∈ ∆(T(Σ)), t t i 4 VALENTINACASTIGLIONI, DANIELGEBLER,ANDSIMONETINI f(π ,...,π ) is the distribution defined by f(π ,...,π )(f(t ,...,t )) = n π (t ). The 1 n 1 n 1 n i=1 i i convexcombination p π ofafamilyofdistributions{π } ⊆ ∆(T(Σ))withp ∈ (0,1] i∈I i i i i∈I Q i and p = 1 is defined by ( p π )(t) = (p π (t)) for all t ∈ T(Σ). i∈I i P i∈I i i i∈I i i P P P 2.2. Bisimulation. A (probabilistic) bisimulation is an equivalence relation over T(Σ) equating two terms if they can mimic each other’s transitions and evolve to distributions related by the same bisimulation. To formalize this intuition, we need to lift relations over terms to relations over distributions. Definition 2 (Relation lifting, [DvG10]). The lifting of a relation R ⊆ T(Σ)×T(Σ) is the relation R† ⊆ ∆(T(Σ))×∆(T(Σ)) with πR†π′ whenever there is a countable set of indexes I such that: (i) π = p δ , (ii) π′ = p δ , and (iii) s R t for all i∈ I. i∈I i si i∈I i ti i i We recall a definition equPivalent to DefinitionP2 which will be useful in the proofs. Proposition 1 ([DD11, Proposition 2.3]). Consider a relation R ⊆ T(Σ)×T(Σ). Then R† ⊆ ∆(T(Σ))×∆(T(Σ)) is the smallest relation satisfying: (1) sRt implies δ R†δ ; s t (2) π R†π′ implies ( p π )R†( p π′), where I is an arbitrary set of indexes i i i∈I i i i∈I i i and p = 1. i∈I i P P Definition P3 (Probabilistic (bi)simulations, [LS91,Seg95b]). AssumeaPTS(T(Σ),A,−→). Then: (1) A binary relation R ⊆ T(Σ)×T(Σ) is a probabilistic simulation if, whenever sRt, if s −→a π then there is a transition t −→a π such that π R†π . s t s t (2) A probabilistic simulation R is a probabilistic ready simulation if, whenever sRt, a a if s −→6 then t −→6 . (3) A probabilistic bisimulation is a symmetric probabilistic simulation. The union of all probabilistic simulations (resp.: ready simulations, bisimulations) is the greatest probabilistic simulation (resp.: ready simulation, bisimulation), denoted by ⊑ (resp.: ⊑ , ∼), called probabilistic similarity (resp.: ready similarity, bisimilarity), and is a r preorder (resp.: preorder, equivalence). 2.3. Logical characterization. As a logic expressing behavioral properties over terms, we consider the modal logic L of [DD11], which extends the Hennessy-Milner Logic [HM85] with a probabilistic choice modality. Definition 4 (Modal logic L, [DD11]). The classes of state formulae Ls and distribution formulae Ld over A are defined by the following BNF-like grammar: Ls: ϕ::= ⊤ | ¬ϕ | ϕ | haiψ j∈J j Ld: ψ ::= i∈IriϕiV where: (i) ϕ,ϕi,ϕj range over Ls, (ii) ψLranges over Ld, (iii) a ∈ A, (iv) J is an at most countable set of indexes with J 6= ∅, and (v) I is an at most countable set of indexes with I 6= ∅, r ∈ (0,1] for each i∈ I and r = 1. i i∈I i We shall write haiϕ for hai i∈PI riϕi with I = {i}, ri = 1 and ϕi = ϕ. Formulae are interpreted over a PTS. L SOS-BASED MODAL DECOMPOSITION ON NONDETERMINISTIC PROBABILISTIC PROCESSES 5 Definition 5 (Semantics of L, [DD11]). Assume a PTS (T(Σ),A,−→). The satisfaction relation |=⊆ (T(Σ)×Ls)∪(∆(T(Σ))×Ld) is defined by structural induction on formulae by • t |= ⊤ always; • t |= ¬ϕ iff t |= ϕ does not hold; • t |= ϕ iff t |= ϕ for all j ∈ J; j∈J j j a • t |= haiψ iff t −→ π for a distribution π ∈ ∆(T(Σ)) with π |= ψ; V • π |= r ϕ iff π = r π for distributions π with t |= ϕ for all t ∈ supp(π ). i∈I i i i∈I i i i i i DealingLwith L is motivatPed by its characterization of bisimilarity, proved in [DD11] (see Theorem 1 below), bisimilarity metric, proved in [CGT16a], and similarity and ready similarity, proved here (see Theorem 2 below). Theorem 1 ([DD11]). Assume an image finite PTS (T(Σ),A,−→) and terms s,t ∈ T(Σ). Then, s∼ t if and only if they satisfy the same formulae in Ls. The characterization of ready similarity and similarity requires two subclasses of L. Definition 6. The class of ready formulae L is defined as r Ls: ϕ::= ⊤ | a¯ | ϕ | haiψ r j∈J j Ld: ψ ::= r ϕ r i∈I iVi where a¯ stays for ¬hai⊤, and the class of positive formulae L are defined as L + Ls : ϕ::= ⊤ | ϕ | haiψ + j∈J j Ld : ψ ::= r ϕ . + i∈VI i i The classes Lr and L+ are strict subloLgics of the one proposed in [DvGHM08] for the characterization offailuresimilarity andforwardsimilarity [Seg95b]. Inparticular, thelogic used in [DvGHM08] allows for arbitrary formulae to occur after the diamond modality. We can show that our sublogics are powerful enough for the characterization of ready similarity and similarity. Theorem 2. Assume an image finite PTS (T(Σ),A,−→) and terms s,t ∈T(Σ). Then: (1) s ⊑ t iff for any formula ϕ ∈Ls, s |= ϕ implies t |= ϕ. r r (2) s ⊑ t iff for any formula ϕ ∈ Ls , s |= ϕ implies t |= ϕ. + Proof. We prove only the first item, namely the characterization of the ready simulation preorder. The proof for simulation is analogous. (⇒) Let ϕ ∈Ls. We aim to prove that r whenever s ⊑ t and s |= ϕ, then t |= ϕ. (2.1) r We proceed by structural induction over ϕ. • Base case ϕ= ⊤. Then the proof obligation Equation (2.1) immediately follows. a • Base case ϕ = a¯. Then, by Definition 5, s |= a¯ gives s −→6 . Since s ⊑ t, this implies r a thatt −→6 from whichwedraw t |= a¯. Therefore, theproofobligation Equation (2.1) follows also in this case. • Inductive step ϕ = ϕ . Then, by Definition 5, s |= ϕ gives that s |= ϕ j∈J j j∈J j j for each j ∈ J. Hence, by structural induction we obtain that t |= ϕ for each j ∈ J, j V V 6 VALENTINACASTIGLIONI, DANIELGEBLER,ANDSIMONETINI thus implying t |= ϕ . Therefore, the proof obligation Equation (2.1) follows j∈J j also in this case. V • Inductive step ϕ = hai r ϕ . Then, by Definition 5, s |= hai r ϕ gives i∈I i i i∈I i i a that there exists a distribution π s.t. s −→ π and π |= r ϕ . Since s ⊑ t, L s s s i∈I i iL r a a † s −→ π implies the existence of a distribution π s.t. t −→ π and π ⊑ π . Hence, s t Lt s r t to derive the proof obligation Equation (2.1) we need to prove that π |= r ϕ . (2.2) t i i i∈I M From π |= r ϕ we gather that π = r π for some distributions π s.t. s i∈I i i s i∈I i i i whenever s′ ∈ supp(π ) then s′ |= ϕ (Definition 5). Moreover, by Definition 2 and i i L P † Proposition 1, π ⊑ π and π = r π together imply the existence of distri- s r t s i∈I i i butions π′ s.t. π = r π′ and for each s′ ∈ supp(π ) there is a t′ ∈ supp(π′) s.t. i t i∈I i i P i i s′ ⊑ t′. Thus, from s′ ⊑ t′ and s′ |= ϕ , structural induction over ϕ gives t′ |= ϕ . r r i i i P Hence, foreach t′ ∈ supp(π′)itholdsthatt′ |= ϕ thusgivingEquation(2.2). There- i i fore, wecan concludethatt |= hai r ϕ andtheproofobligation Equation(2.1) i∈I i i follows also in this case. L (⇐) Assume now that, for any ϕ ∈ Ls, s |= ϕ implies t |= ϕ. We define the relation r R = {(s,t) | s|= ϕ implies t |= ϕ for ϕ ∈Ls}. r We aim to show that R is a probabilistic ready simulation. Let sRt. We aim to prove that b b whenever s −→6 then t −→6 (2.3) whenever s −→a π then there is a transition t −→a π with π R†π . (2.4) s t s t Assume first that s −→6b . Then, by Definition 5, we derive s |=¯b. From sRt we gather t |=¯b b thus giving t −→6 and the proof obligation Equation (2.3) follows. a Next, consider any transition s −→ π . To prove the proof obligation Equation (2.4) we s need to show that there exists a probability distribution π s.t. t −→a π and π R†π . We t t s t recall that by definition of lifting of a relation (Definition 2) we have π R†π iff whenever s t π = p δ , for some set of indexes I, then π = p δ for some processes t s i∈I i si t i∈I i ti i s.t. s Rt for each i ∈ I. Since it is immediate to see that π = π (s′)δ , iP i P s s′∈supp(πs) s s′ by Proposition 1 to prove the proof obligation Equation (2.4) we need to show that there P exists a probability distribution π s.t. π = π (s′)π for a family of probability t t s′∈supp(πs) s s′ distributions {π } s.t. whenever t′ ∈ supp(π ) then s′Rt′. Thus, let us consider s′ s′∈supp(πs) P s′ the set Π = {π |t −→a π ∧ π = π (s′)π ∧ ∃s′ ∈ supp(π ), t′ ∈ supp(π ): s′R6 t′}. t,a s s′ s s′ s′∈sXupp(πs) Our aim is to prove that there is at least one probability distribution π ∈ der(t,a) which t does not belong to the set Π . t,a By construction, for each π ∈ Π there are some processes s′ ∈ supp(π ) and t′ ∈ t,a π s π supp(π ) and a ready state formula ϕ for which s′ |= ϕ but t′ 6|= ϕ . Thus, for each s′π π π π π π SOS-BASED MODAL DECOMPOSITION ON NONDETERMINISTIC PROBABILISTIC PROCESSES 7 s′ ∈ supp(π ) we have s′ |= ϕ . Moreover, for each π ∈ Π with s′ = s′ there s π t,a π {π∈Πt^,a|s′π=s′} is some t′ ∈ supp(π ) s.t. t′ 6|= ϕ . π s′ π π {π∈Πt^,a|s′π=s′} Consider now that ready state formula ϕ = hai π (s′) ϕ . s π s′∈sMupp(πs) {π∈Πt^,a|s′π=s′} Then, it is clear that s |= ϕ thus implying t |= ϕ, as by hypothesis sRt. From t |= ϕ it a follows that there exists a distribution π s.t. t −→ π and t t π |= π (s′) ϕ t s π s′∈sMupp(πs) {π∈Πt^,a|s′π=s′} namely π = π (s′)π′ for some distributions π′ s.t. whenever t′ ∈ supp(π′ ) t s′∈supp(πs) s s′ s′ s′ then t′ |= ϕ . Consequently, π 6∈ Π and hence for all s′ ∈ supp(π ) each P π t t,a s {π∈Πt^,a|s′π=s′} t′ ∈ supp(π′ ) is such that s′Rt′. Therefore, from Proposition 1 we obtain δ R†π′ and s′ s′ s′ consequently (from the same Proposition 1) π R†π , thus proving the proof obligation s t Equation (2.4). 2.4. Probabilistictransitionsystemspecifications. PTSsaremostlydefinedbymeans of SOS rules, which are syntax-driven inference rules allowing us to infer the behavior of terms inductively wrt. their structure. Here we consider rules in the probabilistic GSOS format [DGL14] (examples in Example 2.1), which allow for specifying most of probabilistic process algebras [GLT15, GLT16, GT15]. In these rules we need syntactic expressions that denote probability distributions. We assumea countable set of distribution variables V . We denote by V the setof state and dis- d tribution variables V = V ∪V . We let µ,ν,... range over V and ζ range over V. The set of s d d distribution terms over Σ, V ⊆ V and V ⊆ V , notation DT(Σ,V ,V ), is the least set sat- s s d d s d isfying: (i) {δ | t ∈ T(Σ,V )} ⊆ DT(Σ,V ,V ), (ii) V ⊆ DT(Σ,V ,V ), (iii) f(Θ ,...,Θ )∈ t s s d d s d 1 n DT(Σ,V ,V ) whenever f ∈ Σ and Θ ∈ DT(Σ,V ,V ), and (iv) p Θ ∈ DT(Σ,V ,V ) s d i s d i∈I i i s d whenever Θ ∈ DT(Σ,V ,V ) and p ∈ (0,1] with p = 1. We write DT(Σ) for i s d i i∈I i P DT(Σ,V ,V ), i.e. the set of all open distribution terms, and DT(Σ) for DT(Σ,∅,∅), i.e. s d P the set of all closed distribution terms. Distribution terms have the following meaning. An instantiable Dirac distribution δ t instantiates to δ if t instantiates to t′. A distribution variable µ ∈ V is a variable that t′ d takes values from ∆(T(Σ)). Case (iii) lifts the structural inductive construction of terms to distribution terms. Case (iv) allows us to construct convex combinations of distributions. By var(t) (resp. var(Θ)) we denote the set of the variables occurring in term t (resp. distribution term Θ). a a A positive (resp. negative) literal is an expression of the form t −→ Θ (resp. t −→6 ) with t ∈ T(Σ), a ∈ A and Θ ∈DT(Σ). The literals t −→a Θ and t −→a6 are said to deny each other. 8 VALENTINACASTIGLIONI, DANIELGEBLER,ANDSIMONETINI Definition 7 (PGSOS rules, [DGL14]). A PGSOS rule r has the form: ai,m ai,n {x −−−→ µ | i∈ I,m ∈ M } {x −−−→6 |i ∈ I,n ∈ N } i i,m i i i a f(x ,...,x )−→ Θ 1 n where f ∈ Σ, I = {1,...,n}, M ,N are finite indexes sets, a ,a ,a ∈ A are actions, i i i,m i,n x ∈ V and µ ∈ V are variables and Θ ∈ DT(Σ) is a distribution term. Furthermore, it i s i,m d is required that (i) all µ for i ∈ I and m ∈ M are distinct, (ii) all x ,...,x are distinct, i,m i 1 n and (iii) var(Θ)⊆ {µ |i ∈ I,m ∈ M }∪{x ,...,x }. i,m i 1 n A PGSOS probabilistic transition system specification (PGSOS-PTSS) is a tuple P = (Σ,A,R), with Σ a signature, A a countable set of actions and R a finite set of PGSOS rules. The constraints (i)–(iii) in Definition 7 above, are exactly the constraints of the non- deterministic GSOS format [BIM95] with the difference that we have distribution variables as right hand sides of positive literals. Example 2.1. The operators of synchronous parallel composition | and probabilistic alter- native composition + , with p ∈ (0,1], are specified by the following PGSOS rules: p a a a a a a a a x −→ µ y −→ ν x −→ µ y −→6 x −→6 y −→ ν x −→ µ y −→ ν . a a a a x |y −→ µ | ν x+ y −→ µ x+ y −→ ν x+ y −→ pµ+(1−p)ν p p p For a PGSOS rule r, the positive (resp. negative) literals above the line are the posi- tive premises, notation pprem(r) (resp. negative premises, notation nprem(r)). The literal a f(x ,...,x ) −→ Θ is called the conclusion, notation conc(r), the term f(x ,...,x ) is 1 n 1 n called the source, notation src(r), and the distribution term Θ is called the target, notation trg(r). A PGSOS rule r is said to be positive if nprem(r) = ∅. Then we say that a PGSOS- PTSS P = (Σ,A,R) is positive if all the PGSOS rules in R are positive. A PTS is derived from a PTSS through the notions of substitution and proof. A substitution is a mapping σ: V → T(Σ)∪DT(Σ) such that σ(x) ∈ T(Σ) if x ∈ V and s σ(µ) ∈ DT(Σ) if µ ∈V . It extends to terms, literals and rules by element-wise application. d A substitution is closed if it maps variables to closed terms. A closed substitution instance of a literal (resp. PGSOS rule) is called a closed literal (resp. closed PGSOS rule). Definition 8 (Proof). A proof from a PTSS P = (Σ,A,R) of a closed literal α is a well- founded, upwardly branching tree, with nodes labeled by closed literals, such that the root is labeled α and, if β is the label of a node q and K is the set of labels of the nodes directly above q, then: • either β is positive and K/β is a closed substitution instance of a rule in R, • or β is negative and for each closed substitution instance of a rule in R whose conclusion denies β, a literal in K denies one of its premises. A literal α is provable from P, notation P ⊢ α, if there exists a proof from P of α. We have that each PGSOS-PTSS P is strictly stratifiable [vG96] which implies that P induces a unique model corresponding to the PTS (T(Σ),A,−→) whose transition relation −→ contains exactly the closed positive literals provable from P. Moreover, the existence of a stratification implies that P is also complete [vG96], thus giving that for any term a a t ∈ T(Σ) either P ⊢ t −→ π for some π ∈ ∆(T(Σ)) or P ⊢ t −→6 , namely the PTS induced SOS-BASED MODAL DECOMPOSITION ON NONDETERMINISTIC PROBABILISTIC PROCESSES 9 by P contains literals that do not deny each other [BIM95]. In particular, the notion of provability in Definition 8 (which is called supported in [vG96]) subsumes the negation as failure principle of [Cla77] for the derivation of negative literals: for each closed term t we a a have that P ⊢ t −→6 if and only if P 6⊢ t −→ π for any distribution π ∈ ∆(T(Σ)). 3. Distribution specifications In this section we develop a SOS-like machinery consisting in a set of inference rules, called Σ-distribution rules, through which we syntactically represent open distribution terms as probability distributions over open terms. Informally, these rules allow us to infer the q expression Θ −→ t whenever a closed distribution term Θ assigns probability weight q to a closed term t. More precisely, the idea behind Σ-distribution rules is as follows: assuming that the distribution variable µ is characterized as the distribution {µ −q→i x | i ∈ I} and i the distribution variable ν as the distribution {ν −−q→j x | j ∈J}, the Σ-distribution rule j {µ −q→i x | i∈ I} {ν −−q→j x | j ∈ J} i j {µ | ν −q−i−·q→j x | x i ∈I,j ∈ J} i j allows ustodescribethebehavior ofthedistribut(cid:12)ionterm µ |ν asaprobability distribution (cid:12) over theopenterms x |x . As wewill seein Definition 9below theweights andthepattern i j of the target terms in the conclusion are chosen accordingly to the syntactic structure of the distribution term being the source. For this reason, the Σ-distribution specification, namely the set of Σ-distribution rules on a signature Σ, depends solely on the chosen signature. We also notice that for each possible interpretation of µ and ν as distributions we obtain a different Σ-distribution rule having µ | ν as source. However, we will show that under a suitable notion of provability, the Σ-distribution specification correctly specify the semantics of closed distribution terms. Moreover, our Σ-distribution specification will play a fundamental roˆle in the decomposition method. In fact, in Section 4.2 from the Σ-distribution rules we will derive the Σ-distribution ruloids, which will allow us to derive q expressions of the form Θ −→ t for an arbitrary open distribution term Θ and open term t from the behavior of the variables occurring in Θ. We remark that our Σ-distribution specification can be exploited also to decompose formulae of any logic offering modalities for the specification of the probabilistic properties of processes. Moreover, it can be easily generalized to cover the case of sub-distributions, which are usually considered alongside a weak semantics for processes [LdV15, LdV16]. q 3.1. Σ-distribution rules. A distribution literal is an expression of the form Θ −→ t, with Θ ∈ DT(Σ), q ∈ (0,1] and t ∈ T(Σ). Given a set of (distribution) literals L we denote by lhs(L) the set of the left-hand sides of the (distribution) literals in L and by rhs(L) the set of right-hand sides of the (distribution) literals in L. Aset of distributionliterals {Θ −q→i t | i∈ I} is adistribution over terms if q = 1 i i∈I i andalltermst arepairwisedistinct. Thisexpressesthatthepossiblyopendistributionterm i Θ ∈ DT(Σ)isthedistributionover possiblyopentermsinT(Σ)givingweightq tPot . Given i i an open distribution term Θ ∈ DT(Σ) and a distribution over terms L = {Θ −q→i t | i ∈ I} i we denote the set of terms in rhs(L) by supp(Θ) = {t | i∈ I} ⊆ T(Σ). i 10 VALENTINACASTIGLIONI, DANIELGEBLER,ANDSIMONETINI Our target is to derive distributions over terms {π −q→i t | i ∈ I} for a distribution i π ∈ ∆(T(Σ)) (which coincides with a closed distribution term) and closed terms t ∈ T(Σ) i suchthat: (i){π −q→i t | i∈ I}ifandonlyifπ(t )= q foralli∈ I,and(ii){π −q→i t |i ∈I} i i i i is obtained inductively wrt. the structure of π. To this aim, we introduce the Σ-distribution rules and the Σ-distribution specification. Let δ := {δ | x ∈ V } denote the set of all instantiable Dirac distributions with a Vs x s variable as term, and ϑ,ϑ ,... denote distribution terms in DT(Σ) ranging over V ∪δ . i d Vs ×n Then, for arbitrary sets S ,...,S , we denote by S the set of tuples k = [s ,...,s ] 1 n i=1 i 1 n with s ∈ S . The i-th element of k is denoted by k(i). i i Definition9(Σ-distributionrules). AssumeasignatureΣ. ThesetR oftheΣ-distribution Σ rules consists of the least set containing the following inference rules: (1) 1 {δ −→ x} x for any state variable x ∈ V ; s (2) ϑ −q−i,→j x | j ∈ J i i,j i i=[1,...,nn o f(ϑ ,...,ϑ )−−q→k f(x ,...,x ) k ∈ × J and q = q  1 n 1,k(1) n,k(n) i k i,k(i)  (cid:12) i=1,...,n i=Y1,...,n  (cid:12) where: (cid:12)   (a) f ∈ Σ, (b) the distribution terms ϑ ,...,ϑ are in V ∪δ and are all distinct, 1 n d Vs (c) for each i = 1,...,n the state variables x ’s with j ∈ J are all distinct, i,j i (d) for each i = 1,...,n we have q = 1; j∈Ji i,j P (3) ϑ −q−i,→j x | j ∈ J i i,j i i[∈In o p ϑ −−q→x x x ∈ {x |i ∈ I ∧j ∈J } and q = p ·q i i i,j i x i i,j   Xi∈I (cid:12) i∈I,j∈JiXs.t. xi,j=x  (cid:12) where: (cid:12)   (a) I is an at most countable set of indexes, (b) the distribution terms ϑ with i∈ I are in V ∪δ and are all distinct, i d Vs (c) for each i ∈ I the state variables x ’s with j ∈ J are all distinct, i,j i (d) for each i ∈ I we have q = 1. j∈Ji i,j Then, the Σ-distribution specification (Σ-DS) is defined as the pair D = (Σ,R ). P Σ Σ For each Σ-distribution rule r , all sets above the line are called premises, notation D prem(r ), and the set below the line is called conclusion, notation conc(r ). Then, we D D name the distribution term on the left side of all distribution literals in the conclusion of r D