Sound and Complete axiomatization of trace semantics for probabilistic systems Alexandra Silva1 Ana Sokolova2 1CentrumWiskunde&Informatica(currentlyonleaveatCornellUniv.) 2ComputerSciencesDepartment,UniversityofSalzburg June 2011 Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 1/20 Motivation P:: = 0 | a.P | P +P | µx.Pg Kleene-like theorem: behaviours of LTS are characterized by P’s and vice-versa Axiomatization: P +Q ≡ Q+P;P +0 ≡ P;µx.P ≡ P[µx.P/x];... Soundness and Completeness: P ≡ Q ⇐⇒ P ∼ Q Robin Milner RobinMilner: ACompleteInferenceSystemforaClassofRegularBehaviours. J. Comput. Syst. Sci. 28(3): 439-466(1984) Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 2/20 Motivation P:: = 0 | a.P | P +P | µx.Pg Kleene-like theorem: behaviours of LTS are characterized by P’s and vice-versa Axiomatization: P +Q ≡ Q+P;P +0 ≡ P;µx.P ≡ P[µx.P/x];... Soundness and Completeness: P ≡ Q ⇐⇒ P ∼ Q Robin Milner RobinMilner: ACompleteInferenceSystemforaClassofRegularBehaviours. J. Comput. Syst. Sci. 28(3): 439-466(1984) Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 2/20 Motivation P:: = 0 | a.P | P +P | µx.Pg Kleene-like theorem: behaviours of LTS are characterized by P’s and vice-versa Axiomatization: P +Q ≡ Q+P;P +0 ≡ P;µx.P ≡ P[µx.P/x];... Soundness and Completeness: P ≡ Q ⇐⇒ P ∼ Q Robin Milner RobinMilner: ACompleteInferenceSystemforaClassofRegularBehaviours. J. Comput. Syst. Sci. 28(3): 439-466(1984) Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 2/20 Motivation P:: = 0 | a.P | P +P | µx.Pg Kleene-like theorem: behaviours of LTS are characterized by P’s and vice-versa Axiomatization: P +Q ≡ Q+P;P +0 ≡ P;µx.P ≡ P[µx.P/x];... Soundness and Completeness: P ≡ Q ⇐⇒ P ∼ Q Robin Milner RobinMilner: ACompleteInferenceSystemforaClassofRegularBehaviours. J. Comput. Syst. Sci. 28(3): 439-466(1984) Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 2/20 Motivation Milner’s language + axiomatization + a.P +a.Q ≡ a.(P +Q) Soundness and Completeness: P ≡ Q ⇐⇒ tr(P) = tr(Q) Alexander Rabinovich Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 3/20 Motivation Milner’s language + axiomatization + a.P +a.Q ≡ a.(P +Q) Soundness and Completeness: P ≡ Q ⇐⇒ tr(P) = tr(Q) Alexander Rabinovich Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 3/20 (E (cid:1)E )(cid:1)E ≡E (cid:1)(E (cid:1)E ) 1 2 3 1 2 3 . . . (p ·E)⊕(p ·E)≡(p +p )·E 1 2 1 2 a·(1/2·0⊕1/2·0)(cid:1)a·(1/3·0⊕2/3·0)(cid:1)b·1·0 E::=0|E(cid:1)E|µx.E|x |a·E(cid:48) E(cid:48)::= (cid:76) p ·E i i i∈1···n (cid:80) wherea∈A,p ∈(0,1]and p =1 i i∈1...n i Probabilistic extensions of Milner’s work Segalasystems • a b a 1/2 1/2 2/3 1/3 (cid:3)(cid:3) (cid:27)(cid:27) (cid:3)(cid:3) (cid:27)(cid:27) (cid:15)(cid:15)1 • • • • • Catuscia Palamidessi Yuxin Deng Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 4/20 a·(1/2·0⊕1/2·0)(cid:1)a·(1/3·0⊕2/3·0)(cid:1)b·1·0 (E (cid:1)E )(cid:1)E ≡E (cid:1)(E (cid:1)E ) 1 2 3 1 2 3 . . . (p ·E)⊕(p ·E)≡(p +p )·E 1 2 1 2 Probabilistic extensions of Milner’s work Segalasystems • a b a 1/2 1/2 2/3 1/3 (cid:3)(cid:3) (cid:27)(cid:27) (cid:3)(cid:3) (cid:27)(cid:27) (cid:15)(cid:15)1 • • • • • Catuscia E::=0|E(cid:1)E|µx.E|x |a·E(cid:48) Palamidessi E(cid:48)::= (cid:76) p ·E i i i∈1···n (cid:80) wherea∈A,p ∈(0,1]and p =1 i i∈1...n i Yuxin Deng Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 4/20 (E (cid:1)E )(cid:1)E ≡E (cid:1)(E (cid:1)E ) 1 2 3 1 2 3 . . . (p ·E)⊕(p ·E)≡(p +p )·E 1 2 1 2 Probabilistic extensions of Milner’s work Segalasystems • a b a 1/2 1/2 2/3 1/3 (cid:3)(cid:3) (cid:27)(cid:27) (cid:3)(cid:3) (cid:27)(cid:27) (cid:15)(cid:15)1 • • • • • a·(1/2·0⊕1/2·0)(cid:1)a·(1/3·0⊕2/3·0)(cid:1)b·1·0 Catuscia E::=0|E(cid:1)E|µx.E|x |a·E(cid:48) Palamidessi E(cid:48)::= (cid:76) p ·E i i i∈1···n (cid:80) wherea∈A,p ∈(0,1]and p =1 i i∈1...n i Yuxin Deng Silva&Sokolova (CWI&USalz) SoundandCompleteaxiomatizationoftracesemanticsforprobabilisJtuicnesy2s0te1m1s 4/20