Name
Abstract | ||
|---|---|---|
In this paper, we show how to exploit the structure of some automata-based construction to efficiently solve the LTL synthesis problem. We focus on a construction proposed in Schewe and Finkbeiner that reduces the synthesis problem to a safety game, which can then be solved by computing the solution of the classical fixpoint equation νX.Safe ∩ CPre(X), where CPre(X) are the controllable predecessors of X. We have shown in previous works that the sets computed during the fixpoint algorithm can be equipped with a partial order that allows one to represent them very compactly, by the antichain of their maximal elements. However the computation of CPre(X) cannot be done in polynomial time when X is represented by an antichain (unless P = NP). This motivates the use of SAT solvers to compute CPre(X). Also, we show that the CPre operator can be replaced by a weaker operator CPre crit where the adversary is restricted to play a subset of critical signals. We show that the fixpoints of the two operators coincide, and so, instead of applying iteratively CPre, we can apply iteratively CPre crit. In practice, this leads to important improvements on previous LTL synthesis methods. The reduction to SAT problems and the weakening of the CPre operator into CPre crit and their performance evaluations are new. © 2012 Springer-Verlag. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/s10009-012-0222-5 | STTT |
Keywords | Field | DocType |
antichain algorithms,reactive systems,synthesis,temporal logics | Discrete mathematics,Antichain,Computer science,Automaton,Algorithm,Theoretical computer science,Operator (computer programming),Maximal element,Fixed point,Reactive system,Time complexity,Computation | Journal |
Volume | Issue | ISSN |
15 | 5-6 | 14332787 |
Citations | PageRank | References |
2 | 0.39 | 9 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Emmanuel Filiot | 1 | 217 | 24.98 |
| Naiyong Jin | 2 | 95 | 8.40 |
| Jean-François Raskin | 3 | 1735 | 100.15 |