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:

omega/omega/games/gr1.py

Lines 6 to 18 in 9a3ec0f

	Roderick Bloem, Barbara Jobstmann, Nir Piterman,
	Amir Pnueli, Yaniv Sa'ar
	"Synthesis of reactive(1) designs"
	Journal of Computer and System Sciences
	Vol.78, No.3, pp.911--938, 2012
	Robert Konighofer
	"Debugging formal specifications with
	simplified counterstrategies"
	Master's thesis
	Inst. for Applied Information Processing and Communications,
	Graz University of Technology, 2009

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:

omega/omega/games/gr1.py

Lines 37 to 97 in 9a3ec0f

	def solve_streett_game(aut, rank=1):
	r"""Return winning set and iterants for Streett(1) game.
	The returned value takes into account actions and
	liveness, not initial conditions (i.e., it is the
	fixpoint before reasoning about initial conditions).
	Expects "env" and "sys" players. Writes:
	- `aut.varlist["env'"]`
	- `aut.varlist["sys'"]`
	@param aut: compiled game with <>[] \/ []<> winning
	@type aut: `temporal.Automaton`
	"""
	assert rank == 1, 'only rank 1 supported for now'
	assert aut.bdd.vars or not aut.vars, (
	'first call `Automaton.build`')
	assert len(aut.win['<>[]']) > 0
	assert len(aut.win['[]<>']) > 0
	env_action = aut.action['env']
	sys_action = aut.action['sys']
	aut.build()
	z = aut.true
	zold = None
	while z != zold:
	zold = z
	cox_z = fx.step(env_action, sys_action, z, aut)
	xijk = list()
	yij = list()
	for goal in aut.win['[]<>']:
	goal &= cox_z
	y, yj, xjk = _attractor_under_assumptions(goal, aut)
	z &= y
	xijk.append(xjk)
	yij.append(yj)
	assert is_state_predicate(z), z.support
	return z, yij, xijk
	def _attractor_under_assumptions(goal, aut):
	"""Targeting `goal`, under unconditional assumptions."""
	env_action = aut.action['env']
	sys_action = aut.action['sys']
	xjk = list()
	yj = list()
	y = aut.false
	yold = None
	while y != yold:
	yold = y
	cox_y = fx.step(env_action, sys_action, y, aut)
	unless = cox_y | goal
	xk = list()
	for safe in aut.win['<>[]']:
	x = fx.trap(env_action, sys_action,
	safe, aut, unless=unless)
	xk.append(x)
	y |= x
	yj.append(y)
	xjk.append(xk)
	return y, yj, xjk

and GR(1) synthesis is solved at:

omega/omega/games/gr1.py

Lines 100 to 192 in 9a3ec0f

	def make_streett_transducer(z, yij, xijk, aut):
	"""Return I/O `temporal.Automaton` implementing strategy.
	An auxiliary variable `_goal` is declared,
	to represent the counter of recurrence goals.
	The variable `_goal` is appended to `varlist['impl']`.
	"""
	winning = z
	assert is_realizable(winning, aut)
	_warn_moore_mealy(aut)
	# declare goal counter var
	n_goals = len(aut.win['[]<>'])
	c = '_goal'
	c_max = n_goals - 1
	vrs = {c: (0, c_max)}
	aut.declare_variables(**vrs)
	aut.varlist['sys']
	# compile transducer with refined shared BDD
	env_init = aut.init['env']
	sys_init = aut.init['sys']
	env_action = aut.action['env']
	sys_action = aut.action['sys']
	holds = aut.win['<>[]']
	goals = aut.win['[]<>']
	# compute strategy from iterates
	# \rho_1: switch goals
	rho_1 = aut.false
	for i, goal in enumerate(goals):
	ip = (i + 1) % len(goals)
	s = "({c} = {i}) /\ ({c}' = {ip})".format(c=c, i=i, ip=ip)
	u = aut.add_expr(s)
	u &= goal
	rho_1 |= u
	zstar = _controllable_action(z, aut)
	rho_1 &= zstar
	# \rho_2: descent in basin
	rho_2 = aut.false
	for i, yj in enumerate(yij):
	s = "({c} = {i}) /\ ({c}' = {i})".format(c=c, i=i)
	count = aut.add_expr(s)
	rho_2j = aut.false
	basin = yj[0]
	for y in yj[1:]:
	# steps leading to next basin
	ystar = _controllable_action(basin, aut)
	rim = y & ~ basin
	u = rim & ystar
	rho_2j |= u
	basin |= y
	u = rho_2j & count
	rho_2 |= u
	# \rho_3: persistence holds
	rho_3 = aut.false
	for i, xjk in enumerate(xijk):
	s = "({c} = {i}) /\ ({c}' = {i})".format(c=c, i=i)
	count = aut.add_expr(s)
	rho_3j = aut.false
	used = aut.false
	for xk in xjk:
	assert len(xk) == len(holds), xk
	for x, hold in zip(xk, holds):
	# steps leading to next wait
	xstar = _controllable_action(x, aut)
	stay = x & ~ used
	used |= x
	u = stay & xstar
	u &= hold
	rho_3j |= u
	u = rho_3j & count
	rho_3 |= u
	# \rho
	u = rho_1 | rho_2
	u |= rho_3
	# counter `c` limits
	s = '{c} \in 0..{n}'.format(c=c, n=c_max)
	u &= aut.add_expr(s)
	# `sys_action` is already in the `\rho`
	# next is "useful" only if `env_action` depends on `y'`
	if not aut.plus_one:
	u |= ~ env_action
	if aut.moore:
	u = aut.forall(aut.varlist["env'"], u)
	assert u != aut.false
	symbolic._assert_support_moore(u, aut)
	aut.action['impl'] = u
	aut.varlist['impl'] = list(aut.varlist['sys']) + [c]
	aut.prime_varlists()
	# initial condition for counter
	# (no closure taken for counter)
	s = '{c} = 0'.format(c=c)
	count = aut.add_expr(s)
	_make_init(count, winning, aut)
	return aut.action['impl']

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

omega/spec/Realizability.tla

Lines 1 to 52 in 9a3ec0f

	------------------------- MODULE Realizability -------------------------------
	(* A definition of what it means for a function to realize a property.
	References
	==========
	Ioannis Filippidis, Richard M. Murray
	"Formalizing synthesis in TLA+"
	Technical Report, California Institute of Technology, 2016
	http://resolver.caltech.edu/CaltechCDSTR:2016.004
	Leslie Lamport
	"Miscellany"
	21 April 1991, note sent to TLA mailing list
	http://lamport.org/tla/notes/91-04-21.txt
	*)
	EXTENDS FiniteSets
	IsAFunction(f) == f = [u \in DOMAIN f |-> f[u]]
	IsAFiniteFcn(f) == /\ IsAFunction(f)
	/\ IsFiniteSet(DOMAIN f)
	------------------------- MODULE Inner ---------------------------------------
	VARIABLES x, y
	CONSTANTS f, g, mem0
	Realization(mem, e(_, _)) ==
	LET
	v == << mem, x, y >>
	A == /\ x' = f[v]
	/\ mem' = g[v]
	IN
	/\ mem = mem0
	/\ [][ e(v, v') => A ]_v
	/\ WF_<< mem, x >> ( e(v, v') /\ A)
	Realize(Phi(_, _), e(_, _)) ==
	/\ IsAFiniteFcn(f) /\ IsAFiniteFcn(g)
	/\ (\EE mem: Realization(mem, e)) => Phi(x, y)
	==============================================================================
	Inner(f, g, mem0, x, y) == INSTANCE Inner
	IsARealization(f, g, mem0, Phi(_, _), e(_, _)) ==
	\AA x, y:
	Inner(f, g, mem0, x, y)!Realize(Phi, e)
	IsRealizable(Phi(_, _), e(_, _)) ==
	\E f, g, mem0:
	IsARealization(f, g, mem0, Phi, e)
	==============================================================================

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:

omega/spec/OpenSystems.tla

Lines 53 to 61 in 9a3ec0f

	(* An operator that forms an open system from the closed system that the
	temporal property P(x, y) describes.
	*)
	Unzip(P(_, _), x, y) ==
	LET
	Q(u, v) == P(v, u) (* swap back to x, y *)
	A(u, v) == WhilePlusHalf(Q, Q, v, u) (* swap to y, x *)
	IN
	WhilePlusHalf(A, P, x, y)

[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!