-- 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
-- Maximum 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:
-- Maximize over transitions.
E. 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 maximum reachability probability:
-- Constrain the behavior s.t. for each location there
-- is at least one outgoing transition which must be taken,
-- Realized by: One transition is taken and
-- corresponding guard holds.
-- Location s1:
s1 -> ((guard_trans1 and trans = 1) or
(guard_trans2 and trans = 2));
-- Location s2:
s2 -> (guard_trans3 and trans = 3);
TARGET
-- Note: Target location must have a trivial self loop.
s2;