-- Discrete-time probabilistic hybrid automaton. -- Source: Fränzle, M., Hermanns, H., Teige, T.: Stochastic Satisfiability -- Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid -- Systems. In Egerstedt, M., Mishra, B., eds.: Proceedings of the 11th -- International Conference on Hybrid Systems: Computation and Control -- (HSCC'08). Volume 4981 of Lecture Notes in Computer Science., Springer -- (2008) 172-186 -- Minimum k-bounded reachability probability. DECL -- Locations: boole s1, s2; -- Continuous state components: float [-100,100] y; -- Variables encoding the guards: boole guard_trans1, guard_trans2, guard_trans3; INIT -- Initial state: (s1, y=1.0). s1 and not s2; y = 1.0; DISTR -- Variable encoding non-deterministic choices -- of transitions: -- Minimize over transitions. A. trans {3,2,1}: -- Variables encoding probabilistic choices -- of transitions: R. prob_t1 p = [ 0 -> 0.9, 1 -> 0.1 ]: R. prob_t2 p = [ 0 -> 0.3, 1 -> 0.7 ]: TRANS -- System in exactly one state after transition. s1' + s2' = 1; -- Overapproximation of the system behavior! -- Transition 1 -- Encode guard: guard_trans1 <-> true; -- Impact of probabilistic choice 0 (0.9): (s1 and trans = 1 and prob_t1 = 0 and guard_trans1) -> (y' = 4*y and s1'); -- Impact of probabilistic choice 1 (0.1): (s1 and trans = 1 and prob_t1 = 1 and guard_trans1) -> (y' = y+2 and s2'); -- Transition 2 -- Encode guard: guard_trans2 <-> y >= 4.0; -- Impact of probabilistic choice 0 (0.3): (s1 and trans = 2 and prob_t2 = 0 and guard_trans2) -> (y' = y and s2'); -- Impact of probabilistic choice 1 (0.7): (s1 and trans = 2 and prob_t2 = 1 and guard_trans2) -> (y' = y and s1'); -- Transition 3 (trivial self loop for target location s2) -- Encode guard: guard_trans3 <-> true; -- Impact of transition: (s2 and trans = 3 and guard_trans3) -> (y' = y and s2'); -- For minimum reachability probability: -- Constrain the behavior s.t. for each location there -- is at least one outgoing transition which can be taken, -- Realized by: One guard must hold. -- Location s1: s1 -> (guard_trans1 or guard_trans2); -- Location s2: s2 -> (guard_trans3); TARGET -- Note: Target location must have a trivial self loop. s2;