Below are posts about a selection of the talks of the third and last day of ATVA’14.
Parameterised Synthesis – Roderick Bloem
“A cookie cutter approach to synthesis”
Classical synthesis approach, given a formula synthesise a system (LTL2Verilog). In a classical approach, you do the thinking twice: you write a specification and an implementation, and you verify whether implementation satisfies specification. You do not want to do the same thing twice (use synthesis, see photo). (note: there may be some criticism about this…).
Roderick explains a case study with this classical approach: synthesising the AMBA Arbiter. Some statistics: specification consists of 12 guarantees and 3 assumptions. Problem: size of synthesized system looks exponential in the number of masters involved in the protocol, but size of handwritten implementation is more or less constant (since it is parameterised). The problem is that you are doing monolithic synthesis for the number of masters, so what you want is a cookie-cutter approach, and do parameterised synthesis since real specs are parameterised anyway.
This parameterised approach consists of two steps: (1) synthesis of systems of arbitrary size is reduced to synthesis of fixed size k (adapting cutoff results), and (2) synthesise distributed uniform system of size k. The last problem is undecidable, so you want to use bounded synthesis. We look at both steps in a bit more detail:
- Reduction to fixed size. Example using token rings with Emerson and Namjoshi’s cutoff theorem (from the setting of verification): a ring of size c is correct iff andy ring is correct. If this theorem holds for verification, then it also holds for synthesis so we reuse this sort of result.
- Uniform synthesis. Roderick first looks at parameterised synthesis for token rings with LTL\X specifications which is also undecidable. To tackle this, one can try bounded synthesis (Finkbeiner & Schewe 2007) instead. For bounded synthesis there is a semi-decision procedure which basically repeatedly tries to find a small implementation that satisfies the formula; if such a thing exists it terminates with the smallest implementation. The approach uses nice automata theoretic results such as one-letter co-Buechi universality. The actual synthesis is performed using an SMT solver. This bounded synthesis approach is then generalised to uniform synthesis, again giving a semi-decision procedure.
All of the above is explained for the token ring problem. Roderick goes on to show the whole approach in a more general setting, the ideas are similar, but the cutoffs not only depend on the property but also on the size of the system, so the whole approach is a bit more complex. All this is implemented in the tool PARTY (but only works for very simple examples).
Some additional observations on synthesis that are interesting to mention:
- Only safety is not enough for synthesis
- You have to do liveness as well
- For this you want to take fairness into account
To conclude this post: of course, the cookie cutter in the talk is in the uniformity of the process: you make a template (the cookie cutter) to build a ring in which all processes are the same!
Fast Debugging of PRISM Models – Christian Dehnert
For the talk, Christian focuses on debugging probabilistic reachability properties on probabilistic automata, although the approach is a bit more general than that. The work is done in the context of PRISM, hence models are described in its modelling language; the state space is essentially the cartesian product of the variables in the model.
Giving high-level counterexamples in terms of commands is NP-hard; an existing approach by Wimmer computing a minimal set of commands takes a long time for realistic examples. In the current talk, they describe a new approach. The proposed approach is to enumerate all command sets while cutting away sub-optimals sets (because otherwise the number of sets is large). In the approach constraints are created eliminating these unwanted counterexamples, and all this is encoded into a MaxSAT problem.
Verification of Markov Decision Processes using Learning Algorithms – Jan Kretinsky
How can we benefit from results from the machine learning community in probabilistic verification? This is the central question of Jan’s talk. He illustrates the approach using LTL model checking of MDPs. The problem in practice is that computing reachability of maximal end components is too slow. Jan proposes heuristics from machine learning to compute this reachability.
The heuristics are applied to the fixed point computation in value iteration. What are the heuristics? Observe that stabilisation of fixed point computation depends on the order of evaluation. The idea is to more frequently evaluate states that are visited more frequently by good schedulers. They use reinforcement learning for this. The same idea is also applied to the case where you don’t know the exact transitions in a statistical model checking setting.
Rabinizer 3 – Jan Kretinsky
The translation from LTL to non-det. BA and from non-det. BA to det. Rabin automaton are both exponential, and both translations are traditionally needed in the verification of LTL formulae. Determination is complicated, results in a “messy” state space, and is hard to implement. Therefore, there are results that try to get rid of this determinisation step. Existing translations (e.g. in Rabinizer and Rabinizer 2) go directly from LTL to DRA without making this determinisation step. In this talk, Jan presents a method that translates the whole of LTL to deterministic (transition-based) generalised Rabin automata (DTGRA). These are as easy to use for probabilistic model checking than DRA, yet do not blow up so bad; using them for synthesis is more complicated.
A Game-Theoretic Approach to Simulation of Data-Parameterised Systems – Sharai Sheinvald
The final session of ATVA is kicked off by Sharai, one of my fellow students of the Marktoberdorf Summerschool in 2011.
Data-parameterised systems are finite state systems with variables, that can range over infinite domains, so clearly describe infinite state systems using a finite representation. For data-parameterised systems, Sharai extends temporal logic with variables to variable temporal logic (VTL); this is simply a first-order extension for LTL likewise she extends CTL* to VCTL*, a first order extension of CTL*.
Traditionally we know that ACTL* characterises simulation. Sharai’s contribution is a simulation definition for abstract systems, with and algorithm for finding such a simulation, and a game-based characterisation. To take care of the data parameterisation, the simulation relation is extended with a function matching the variables between the different systems. Finding the maximal simulation is exponential — in this setting language equivalence is exponential though. If games are related using simulation than they satisfy the same VACTL* formulas, lifting the results for the non-parameterised case. There also is a simulation game between refuter and prover such that games are related iff prover has a memoryless winning strategy in this simulation game. Likewise, if there is no simulation relation, than refuter has a memoryless winning strategy. In both cases some information about variables needs to be remembered though. A nice result in addition is that if there is no simulation relation between to systems, then there is a distinguishing VACTL formula.
Symmetry Reduction in Infinite Games with Finite Branching – Steen Vester
This is the last talk of the conference. We all know very well that parity games, once we generate them explicitly, get very large. Steen tries to attack this by defining symmetry reduction on games. The results work for infinite games with finite branching due to the application of Koenigs lemma in the proofs. The symmetry approach is the same as the classical symmetry approach for labelled transition systems or Kripke structures, based on symmetry groups and orbits. The symmetry results is proved for general objectives. As examples he instantiates the results for parity games and to alternating temporal logic. For concurrent games, the approach also works, but symmetries must map actions to actions.
An interesting open question about this work is whether this can be generalised to infinite games in which we also allow finite branching.
ATVA 2015 will be held in Shanghai. Abstracts need to be submitted by April 22, 2015.