TLSF initial conditions in synthesized AIGER circuits?

[johnyf]

In SYNTCOMP 2014 and 2015, both input and output formats were in AIGER. There was a unique initial state for the latch variables (all zero, p.5). The inputs Xu and outputs Xc were not part of the state mentioned in the (implicitly meant) temporal property [] ! BAD.

So, the transition relation was T(L, Xu, Xc, L'). In a temporal logic with variable priming interpreted as in typical GR(1) studies, this transition relation would be written L' = f(L, Xu', Xc').
For this reason, the resulting controller never had to read Xu or Xc (the previous values of input and output variables). It just read Xu' and Xc' (in the logic), which were Xu and Xc (in the AIGER circuit). The initial conditions of Xu and Xc were altogether ignored (equiv., Xu and Xc were considered "actions").

What interpretation will be given to TLSF for GR(1)?
How do the initial conditions of TLSF correspond to the AIGER circuit synthesized?

The situation is different when TLSF is given as input, instead of AIGER. A TLSF property mentions the variables Xu and Xc (so not only BAD), and the synthesized result will be a transition relation that reads Xu, Xu', Xc and outputs Xc'. For the transition relation to not mention Xc, it must be the case that Xc doesn't appear in the TLSF property, which is a contradiction, in contrast to synthesis from AIGER input.

Therefore, the synthesized AIGER circuit has to somehow read Xu, Xu', Xc'. If the AIGER inputs are only Xu' and the outputs only Xc', then the synthesizer has to add latches for remembering the previous values Xu and Xc. But then the latches should have names Xu and Xc, and the AIGER inputs Xu' and the AIGER outputs coincide with the latches Xc. Otherwise, the AIGER execution wouldn't correspond to the temporal property in TLSF, because it would miss the initial state (equal to the initial values of the latches Xu and Xc).

Is this the case? Does this imply that the synthesizers should necessarily have to define these latches, so that the model checker can decide whether the TLSF property holds?

Will it be necessary to define as outputs also the Xu latches? Also, the Xu' inputs can be named Xu too, but with the understanding that the TLSF property will refer to the Xu latches, not to the Xu input signals to the AIGER circuit.

An alternative would be to read the initial values, by dedicating one "round" of AIGER execution to store these values as the "previous" ones (i.e., to "initialize" the circuit). But that would mean that the first step of the AIGER circuit should be omitted, and the second AIGER step is the first TLSF step (from initial TLSF values to second state in the temporal logic sequence).

Initial condition

Assuming that the synthesizer defines the latches Xu and Xc, there remains the matter of initial conditions. If the SYNTCOMP 2014 assumption remains, that there is a unique initial condition 0, then the synthesizer will assume that Xu and Xc are initially zero, and that would correspond to those latches being zero.

This zero initial condition would have to appear in TLSF. Otherwise, in case TLSF describes a more liberal initial condition (multiple initial states), then the SYNTCOMP 2014 assumption that the latches are initially zero does not hold any more.

From these two alternatives, which one will be used in SYNTCOMP 2016?

[swenjacobs]

I'm not sure that I understand the problem completely, but I'll try to clarify. Let me know if this answers your questions:

1. Indeed, when going beyond pure safety (such as GR(1) or full LTL), the synthesized circuit may need to remember previous inputs. (for safety this is not necessary, since it allows memoryless strategies, and therefore the controllers for specifications in AIGER format can depend only on current inputs and the state of the pre-defined latches)
2. Yes, we still assume that all latches are initialized to 0.
3. From my perspective (correct me if I'm wrong), this is not a problem, because the specification does not talk about the latches directly, but only about inputs and outputs of the synthesized circuit. Therefore, the synthesizer can always produce a circuit that provides the necessary outputs, regardless of the initialization of the latches (assuming that the specification is realizable). If your outputs should directly depend on the stored value of a previous input, but the initialization value would produce an output that does not satisfy the specification, you can always work around this by modifying the circuit. Such a circuit could use a different valuation of outputs in the initial step, e.g., by having one auxiliary latch that remembers whether this is the initial state or not.