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.
Similar content being viewed by others
References
Acacia. http://www.antichains.be/acacia
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: International Conference on Automata, Languages and Programming (ICALP) (1989)
Bloem R., Galler S., Jobstmann B., Piterman N., Pnueli A., Weiglhofer M.: Specify, compile, run: hardware from psl. Electr. Notes Theor. Comput. Sci. 190(4), 3–16 (2007)
Ehlers, R.: Symbolic bounded synthesis. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 6174, pp. 365–379. Springer, Berlin (2010)
Eén, N., Sörensson, N.: MiniSat. http://minisat.se/ (2010)
Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, vol 5643, pp. 263–277. Springer, Berlin (2009)
Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 112–127 (2010)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Proceedings of the International Conference on Computer Aided Verification (CAV). LNCS, pp. 53–65. Springer, Berlin (2001)
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 117–124. IEEE Computer Society (2006)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: IEEE Symposium on Foundations of Computer Science (FOCS) (2005)
Lily. http://www.iaik.tugraz.at/content/research/design_verification/lily/
Martin, D.: Borel determinacy. In: Annals of Mathematics, vol. 102, pp. 363–371 (1975)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symposium on Principles of Programming Languages (POPL). ACM, New York 1989
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Proceedings of 16th ICALP, 1989
Safra, S.: On the complexity of ω automata. In: IEEE Symposium on Foundations of Computer Science (FOCS), pp. 319–327 (1988)
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). LNCS, vol 4762, pp. 474–488. Springer, Berlin (2007)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Proceedings of the International Conference on Computer Aided Verification (CAV) (2000)
Thomas, W.: Church’s problem and a tour through automata theory. In: Pillars of Computer Science. LNCS, vol 4800, pp 635–655. Springer, Berlin (2008)
Wring. http://www.iaik.tugraz.at/content/research/design_verification/wring/
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Filiot, E., Jin, N. & Raskin, JF. Exploiting structure in LTL synthesis. Int J Softw Tools Technol Transfer 15, 541–561 (2013). https://doi.org/10.1007/s10009-012-0222-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-012-0222-5