Product DTMC + LTL property with transition probabilities greater than 1

[anice...@gmail.com]

Hi all,

I use PRISM to extract the product between a DTMC and the DFA corresponding to an LTL property thank to the following command:

prism -importmodel example.tra,lab,sat example.pctl -dtmc  -exportprodtrans example_prod.tra -exportprodstates example_prod.sta -exporttarget example_prod.lab

When I look to the file example_prod.tra I have transitions with probabilities greater than one. I do not understand what it means. The product is not supposed to be a Markov Chain?

example_prod.tra content:

4 5

0 0 16.8

0 2 11.2

1 1 49

2 1 49

3 0 1

PRISM output :

Importing model (DTMC) from "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast.tra", "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast.sta", "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast.lab"...

Parsing properties file "data/ltl_property/inputs/probabilistic_broadcast.pctl"...

1 property:

(1) P=? [ (F hello&(X F hello)) ]

Building model...

Computing reachable states...

Reachability (BFS): 3 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.018 seconds.

Type:        DTMC

States:      3 (1 initial)

Transitions: 4

Transition matrix: 13 nodes (5 terminal), 4 minterms, vars: 2r/2c

---------------------------------------------------------------------

Model checking: P=? [ (F hello&(X F hello)) ]

Building deterministic automaton (for (F "L0"&(X F "L0")))...

DFA has 3 states, 1 goal states.

Time for deterministic automaton translation: 0.079 seconds.

Constructing MC-DFA product...

Reachability (BFS): 2 iterations in 0.00 seconds (average 0.000000, setup 0.00)

States:      4 (1 initial)

Transitions: 5

Transition matrix: 28 nodes (5 terminal), 5 minterms, vars: 4r/4c

Exporting product transition matrix to file "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast_ltl.tra"...

Exporting product state space to file "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast_ltl.sta"...

Skipping BSCC computation since acceptance is defined via goal states...

Computing reachability probabilities...

Exporting target states info to file "/Users/Anicet/Documents/These/Depots/pimc_pylib/data/ltl_property/outputs/tmp/probabilistic_broadcast_ltl.lab"...

Prob0: 4 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Prob1: 1 iterations in 0.00 seconds (average 0.000000, setup 0.00)

yes = 4, no = 0, maybe = 0

Value in the initial state: 1.0

Time for model checking: 0.092 seconds.

Result: 1.0 (value in the initial state)

Cordially,

Anicet