sjunges
commented
5 years ago Naturally, the problem statement is different whether you restrict to graph-preserving valuations or not, see e.g., http://arxiv.org/abs/1904.01503. However, for computing a solution function, it generally does not make sense from a theoretical perspective to disable them as there is no longer a rational function closed form. For a more computational explanation, see e.g., http://arxiv.org/abs/1903.07993.
When you are referring to synthesising a strategy, this is vague, as we are considering DTMCs in your example. I guess you refer to computing a strategy for POMDPs as the connection pointed out in http://auai.org/uai2018/proceedings/papers/195.pdf. That paper also points out this particular problem, and gives some hints about the continuity of the function---later rephrased in the literature pointed to above.
I fail to comprehend the paragraph from "There is... these constraints".
I also fail to comprehend how we should switch these constraints off, and what kind of output you would expect.
In some use cases it may not be desirable to preserve the graph of a pMC.
For example, when using storm-pars go check the property
P=? [ G ! crash ]on the following modelThe result of the query is 0 (as is shown below).
The result is 0 since a graph-preserving constrain prohibits p1 = 1. However, when synthesizing an optimal strategy for this problem it may not be necessary to keep the transition from state 0 to 1 as a possibility.
There is of course a workaround by using z3 only on the well-formedness constraints, but it would be nice if storm-pars also offered the possibility to disable the graph-preserving constraints. In addition, it may not always be easy to determine which formula to optimize under these constraints.
My theoretical knowledge is not deep enough to know if this causes problems in some other cases (since it may cause graph components to become disconnected).