Understand synthesize algorithms ()

[DangMinh24]

Hi all,

I am quite new to LTL specification, and trying to understand the idea of synthesizing. As far as I understand, synthesizing is the process building controller/automata/strategy that can satisfies predefined GR(1) specification. But I can not find any sample document about such procedure.

Could anyone please help with some reference? Much appreciate

[johnyf]

Indeed, synthesis is the construction of an implementation that satisfies a given temporal logic specification. The specification usually includes liveness formulas, and these formulas may be in GR(1) form (generalized reactivitiy of rank 1), or generalized Rabin of rank 1, or other (synthesis for the first two forms is implemented in omega). An implementation can be represented in various ways, one representation is as a formula. In this case a synthesized implementation is such that it implies the given specification, and also includes a much simpler liveness condition (when represented in TLA+).

For GR(1) synthesis, please consult the paper "Synthesis of reactive(1) designs" by Piterman, Pnueli, and Sa'ar, and the references cited in the docstring of the module omega.games.gr1:

https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/omega/games/gr1.py#L6-L18

The documentation of omega includes a discussion of synthesis, and can be found at: https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/doc/doc.md . Studying the module omega.games.gr1 would also be useful. GR(1) realizability (the problem of whether there exists an implementation) is solved at:

https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/omega/games/gr1.py#L37-L97

and GR(1) synthesis is solved at:

https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/omega/games/gr1.py#L100-L192

What realizability means can be understood by reading the TLA+ module Realizability and the references therein:

https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/spec/Realizability.tla#L1-L52

For learning TLA+ the book to study is "Specifying systems" by Lamport.

An introduction to synthesis and the material in the TLA+ modules Realizability and OpenSystems (mentioned below) can be found in the paper "Layering assume-guarantee contracts for hierarchical system design" and the dissertation "Decomposing formal specifications Into assume-guarantee contracts for hierarchical system design".

Please note that temporal logic specifications for synthesis are in a particular form that is obtained by using suitable temporal operators for defining open systems, for example the operator Unzip:

https://github.com/tulip-control/omega/blob/9a3ec0f236900fd976c75ca5f332803c233dab23/spec/OpenSystems.tla#L53-L61

[DangMinh24]

Thank you so much @johnyf for amazing references! Help me a lot in understanding the big picture.

Please correct me if I'm wrong: Is the big picture of GR(1) synthesizing procedure, is to use properties of predefined specification (init, safety, liveness) to construct back an strategy in form

Component == Init /\ [] ImplNext

that also satifies theorem

THEOREM Component => Spec?

I am extremely curious in how such construction can satisfy (soundness). Is BDD is a standard way to describe such procedure? Is it possible to have an equivalent one with non-BDD use (easier to analyze soundness)?

[johnyf]

Yes, this is a high-level description of the synthesis problem.

Binary decision diargams (BDDs) are one way to represent the problem (also called symbolic). Yes, an equivalent approach with an enumerated representation is possible, and the Python package gr1py https://pypi.org/project/gr1py/ is an implementation of enumerative synthesis from GR(1) specifications.

About proofs of correctness for GR(1) synthesis, in addition to the above references, please consult the paper "Bridging the gap between fair simulation and trace inclusion" by Kesten, Piterman, and Pnueli, in particular Appendix B.

A tutorial paper with material about GR(1) synthesis, attractor computations, and binary decision diagrams is "Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox".

The fixpoint algorithm for computing realizability is similar in the enumerative and symbolic implementations (the enumerative implementation can be found in the module gr1py.solve https://github.com/slivingston/gr1py/blob/debbd78eb6788d2bec4752d76a2bc38972971d4b/gr1py/solve.py#L32-L86). The main difference is in how sets of states and transitions are represented and reasoned about computationally.

[DangMinh24]

Thank you so much for such kind explanations @johnyf!