[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Efficient Reactive Synthesis Using Mode Decomposition

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2023 (ICTAC 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14446))

Included in the following conference series:

Abstract

Developing critical components, such as mission controllers or embedded systems, is a challenging task. Reactive synthesis is a technique to automatically produce correct controllers. Given a high-level specification written in LTL, reactive synthesis consists of computing a system that satisfies the specification as long as the environment respects the assumptions. Unfortunately, LTL synthesis suffers from high computational complexity which precludes its use for many large cases.

A promising approach to improve synthesis scalability consists of decomposing a safety specification into a smaller specifications, that can be processed independently and composed into a solution for the original specification. Previous decomposition methods focus on identifying independent parts of the specification whose systems are combined via simultaneous execution.

In this work, we propose a novel decomposition algorithm based on modes, which consists on decomposing a complex safety specification into smaller problems whose solution is then composed sequentially (instead of simultaneously). The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable then the full specification is realizable. Moreover, we show how to construct a system for the original specification from sub-systems for the decomposed specifications. We finally illustrate the feasibility of our approach with multiple cases studies using off-the-self synthesis tools to process the obtained sub-problems.

Funded by PRODIGY Project (TED2021-132464B-I00)—funded by MCIN/AEI/ 10.13039/501100011033 and the EU NextGenerationEU/PRTR—,by DECO Project (PID2022-138072OB-I00)—funded by MCIN/AEI/10.13039/501100011033 and by the ESF+—and by a research grant from Nomadic Labs and the Tezos Foundation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 51.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 64.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. The reactive synthesis competition. https://www.syntcomp.org/

  2. Alur, R., Torre, S.L.: Deterministic generators and games for LTL fragments. In: Proceedings of the LICS’01, pp. 291–300. ACM (2001)

    Google Scholar 

  3. Balachander, M., Filiot, E., Raskin, J.F.: LTL reactive synthesis with a few hints. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. LNCS, vol. 13994, pp. 309–328. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30820-8_20

  4. Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI’20 (2020)

    Google Scholar 

  5. Bharadwaj, R., Heitmeyer, C.: Applying the SCR requirements method to a simple autopilot. In: NASA Conference Publication, pp. 87–102. NASA (1997)

    Google Scholar 

  6. Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. JCSS 78(3), 911–938 (2012)

    MathSciNet  MATH  Google Scholar 

  7. Brizzio, M., Cordy, M., Papadakis, M., Sánchez, C., Aguirre, N., Degiovanni, R.: Automated repair of unrealisable LTL specifications guided by model counting. In: Proceedings of the GECCO’23, pp. 1499–1507. ACM (2023)

    Google Scholar 

  8. Bultan, T.: Action language: a specification language for model checking reactive systems. In: In: Proceedings of the ICSE, pp. 335–344 (2000)

    Google Scholar 

  9. Carvalho, L., et al.: ACoRe: automated goal-conflict resolution. In: In: Proceedings of the FASE’23 (2023)

    Google Scholar 

  10. Chang, E., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474–486. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55719-9_97

    Chapter  Google Scholar 

  11. Church, A.: Logic, arithmetic, and automata (1962)

    Google Scholar 

  12. Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Log. 28(4), 289–290 (1963). https://doi.org/10.2307/2271310

  13. De Giacomo, G., Favorito, M.: Compositional approach to translate LTLf/LDLf into deterministic finite automata. In: Proceedings of the ICAPS’21, pp. 122–130 (2021)

    Google Scholar 

  14. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the IJCAI’13, pp. 854–860. AAAI Press (2013)

    Google Scholar 

  15. Degiovanni, R., Castro, P.F., Arroyo, M., Ruiz, M., Aguirre, N., Frias, M.F.: Goal-conflict likelihood assessment based on model counting. In: ICSE (2018)

    Google Scholar 

  16. Degiovanni, R., Ponzio, P., Aguirre, N., Frias, M.: Improving lazy abstraction for SCR specifications through constraint relaxation. STVR 28(2), e1657 (2018)

    Google Scholar 

  17. D’ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol. 22(1) 1–36 (2013). https://doi.org/10.1145/2430536.2430543

  18. Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies (\(D^{3}\)). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309–327. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_17

    Chapter  Google Scholar 

  19. Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 333–339. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_18

    Chapter  Google Scholar 

  20. Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)

    Article  MATH  Google Scholar 

  21. Esparza, J., Křetínský, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192–208. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_13

    Chapter  Google Scholar 

  22. Fifarek, A., Wagner, L., Hoffman, J., Rodes, B., Aiello, A., Davis, J.: SpeAR v2.0: formalized past LTL specification and analysis of requirements. In: NFM (2017)

    Google Scholar 

  23. Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 112–127. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15643-4_10

    Chapter  MATH  Google Scholar 

  24. Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. ISSE (2022)

    Google Scholar 

  25. Finucane, C.P., Jing, G., Kress-Gazit, H.: Designing reactive robot controllers with LTLMoP. In: Proceedings of the AAAIWS’11 (2011)

    Google Scholar 

  26. Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Nija, S.: Formal requirements elicitation with FRET. In: REFSQ’20 (2020)

    Google Scholar 

  27. Heitmeyer, C.: Requirements models for critical systems. In: Software and Systems Safety, pp. 158–181. IOS Press (2011)

    Google Scholar 

  28. Heitmeyer, C., Labaw, B., Kiskis, D.: Consistency checking of SCR-style requirements specifications. In: Proceedings of the RE’95, pp. 56–63. IEEE (1995)

    Google Scholar 

  29. Heitmeyer, C., et al.: Building high assurance human-centric decision systems. AuSE 22, 159–197 (2015)

    Google Scholar 

  30. Heitmeyer, C.L., McLean, J.D.: Abstract requirements specification: a new approach and its application. IEEE TSE 5, 580–589 (1983)

    Google Scholar 

  31. Heninger, K.L.: Software requirements for the a-7e aircraft. NRL Memorandum Report 3876, Naval Research Laboratory (1978)

    Google Scholar 

  32. Hermo, M., Lucio, P., Sánchez, C.: Tableaux for realizability of safety specifications. In: Proceedings of the FM’23, pp. 495–513 (2023)

    Google Scholar 

  33. Iannopollo, A., Tripakis, S., Vincentelli, A.: Specification decomposition for synthesis from libraries of LTL assume/guarantee contracts. In: DATE. IEEE (2018)

    Google Scholar 

  34. Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. EPTCS 229, 112–132, November 2016

    Google Scholar 

  35. Kirby, J.: Example NRL SCR software requirements for an automobile cruise control and monitoring system. Wang Inst. of Graduate Studies (1987)

    Google Scholar 

  36. Kress-Gazit, H., Wongpiromsarn, T., Topcu, U.: Correct, reactive, high-level robot control. IEEE Robot. Autom. Mag. 18(3), 65–74 (2011)

    Article  Google Scholar 

  37. Křetínský, J., Meggendorfer, T., Sickert, S.: Owl: a library for \(\omega \)-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543–550. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_34

    Chapter  MATH  Google Scholar 

  38. Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: SOFSEM’12 (2012)

    Google Scholar 

  39. Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_6

    Chapter  Google Scholar 

  40. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19, 291–314 (2001)

    Article  MATH  Google Scholar 

  41. Letier, E., Kramer, J., Magee, J., Uchitel, S.: Deriving event-based transition systems from goal-oriented requirements models. AuSE 15, 175–206 (2008)

    Google Scholar 

  42. Li, J., Pu, G., Zhang, L., Yao, Y., Vardi, M.Y., He, J.: Polsat: a portfolio LTL satisfiability solver (2013). http://arxiv.org/abs/1311.1602

  43. Mallozzi, P., Incer, I., Nuzzo, P., Sangiovanni-Vincentelli, A.L.: Contract-based specification refinement and repair for mission planning. In: FormaliSE’23 (2023)

    Google Scholar 

  44. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, NY, USA (1995). https://doi.org/10.1007/978-1-4612-4222-2

  45. Mavin, A., Wilkinson, P., Harwood, A., Novak, M.: Easy approach to requirements syntax (EARS), pp. 317–322, October 2009. https://doi.org/10.1109/RE.2009.9

  46. Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578–586. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_31

    Chapter  Google Scholar 

  47. Pnueli, A.: The temporal logic of programs. In: SFCS’77, pp. 46–57. IEEE (1977)

    Google Scholar 

  48. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’89), pp. 179–190 (1989). https://doi.org/10.1145/75277.75293

  49. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_38

    Chapter  Google Scholar 

  50. de Roever, W.P., Langmaack, H., Pnueli, A. (eds.): Compositionality: The Significant Difference. Springer, Berlin, Heidelberg (1998). https://doi.org/10.1007/3-540-49213-5

  51. van Schouwen, A.J., Parnas, D.L., Madey, J.: Documentation of requirements for computer systems. In: Proceedings of the ISRE, pp. 198–207. IEEE (1993)

    Google Scholar 

  52. Sistla, A.P.: Safety, liveness, and fairness in temporal logic. FAC 6, 495–511 (1994)

    MATH  Google Scholar 

  53. Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety LTL synthesis. In: HVC 2017. LNCS, vol. 10629, pp. 147–162. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70389-3_10

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Matías Brizzio & César Sánchez

  2. Universidad Politécnica de Madrid, Madrid, Spain

    Matías Brizzio

Authors
  1. Matías Brizzio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. César Sánchez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to César Sánchez .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Erika Ábrahám

  2. Eindhoven University of Technology, Eindhoven, The Netherlands

    Clemens Dubslaff

  3. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Brizzio, M., Sánchez, C. (2023). Efficient Reactive Synthesis Using Mode Decomposition. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T. (eds) Theoretical Aspects of Computing – ICTAC 2023. ICTAC 2023. Lecture Notes in Computer Science, vol 14446. Springer, Cham. https://doi.org/10.1007/978-3-031-47963-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-47963-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-47962-5

  • Online ISBN: 978-3-031-47963-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation