skip to main content
10.1145/3106237.3106240acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
research-article

A symbolic justice violations transition system for unrealizable GR(1) specifications

Published: 21 August 2017 Publication History

Abstract

One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. Existing approaches to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, include the generation of concrete counter-strategies and the computation of an unrealizable core. Although correct, such approaches produce large and complicated counter-strategies, often containing thousands of states. This hinders their use by engineers.
In this work we present the Justice Violations Transition System (JVTS), a novel symbolic representation of counter-strategies for GR(1). The JVTS is much smaller and simpler than its corresponding concrete counter-strategy. Moreover, it is annotated with invariants that explain how the counter-strategy forces the system to violate the specification. We compute the JVTS symbolically, and thus more efficiently, without the expensive enumeration of concrete states. Finally, we provide the JVTS with an on-demand interactive concrete and symbolic play.
We implemented our work, validated its correctness, and evaluated it on 14 unrealizable specifications of autonomous Lego robots as well as on benchmarks from the literature. The evaluation shows not only that the JVTS is in most cases much smaller than the corresponding concrete counter-strategy, but also that its computation is faster.

References

[1]
R. Alur, S. Moarref, and U. Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In FMCAD, pages 26–33. IEEE, 2013.
[2]
R. Bloem, A. Cimatti, K. Greimel, G. Hofferek, R. Könighofer, M. Roveri, V. Schuppan, and R. Seeber. RATSY - A new requirements analysis tool with synthesis. In CAV, volume 6174 of LNCS, pages 425–429. Springer, 2010.
[3]
R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa’ar. Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci., 78(3):911–938, 2012.
[4]
A. Cimatti, M. Roveri, V. Schuppan, and A. Tchaltsev. Diagnostic information for realizability. In VMCAI, volume 4905 of LNCS, pages 52–67. Springer, 2008.
[5]
N. D’Ippolito, V. A. Braberman, N. Piterman, and S. Uchitel. Synthesis of live behaviour models for fallible domains. In ICSE, pages 211–220, 2011.
[6]
N. D’Ippolito, V. A. Braberman, N. Piterman, and S. Uchitel. Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol., 22(1):9, 2013.
[7]
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In ICSE, pages 411–420. ACM, 1999.
[8]
R. Ehlers and V. Raman. Slugs: Extensible GR(1) synthesis. In CAV, volume 9780 of LNCS, pages 333–339. Springer, 2016.
[9]
I. Filippidis, S. Dathathri, S. C. Livingston, N. Ozay, and R. M. Murray. Control design for hybrid systems with tulip: The temporal logic planning toolbox. In 2016 IEEE Conference on Control Applications, CCA 2016, Buenos Aires, Argentina, September 19-22, 2016, pages 1030–1041. IEEE, 2016.
[10]
R. Könighofer, G. Hofferek, and R. Bloem. Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT, 15(5-6):563–583, 2013.
[11]
H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics, 25(6):1370–1381, 2009.
[12]
S. Maniatopoulos, P. Schillinger, V. Pong, D. C. Conner, and H. Kress-Gazit. Reactive high-level behavior synthesis for an atlas humanoid robot. In D. Kragic, A. Bicchi, and A. D. Luca, editors, 2016 IEEE International Conference on Robotics and Automation, ICRA 2016, Stockholm, Sweden, May 16-21, 2016, pages 4192–4199. IEEE, 2016.
[13]
S. Maoz and J. O. Ringert. GR(1) synthesis for LTL specification patterns. In ESEC/FSE, pages 96–106. ACM, 2015.
[14]
S. Maoz and J. O. Ringert. On well-separation of GR(1) specifications. In FSE, pages 362–372. ACM, 2016.
[15]
S. Maoz and Y. Sa’ar. AspectLTL: an aspect language for LTL specifications. In AOSD, pages 19–30. ACM, 2011.
[16]
S. Maoz and Y. Sa’ar. Assume-guarantee scenarios: Semantics and synthesis. In MODELS, volume 7590 of LNCS, pages 335–351. Springer, 2012.
[17]
S. Maoz and Y. Sa’ar. Counter play-out: executing unrealizable scenario-based specifications. In ICSE, pages 242–251. IEEE / ACM, 2013.
[18]
S. Maoz and Y. Sa’ar. Two-way traceability and conflict debugging for aspectltl programs. T. Aspect-Oriented Software Development, 10:39–72, 2013.
[19]
N. Piterman, A. Pnueli, and Y. Sa’ar. Synthesis of reactive(1) designs. In VMCAI, volume 3855 of LNCS, pages 364–380. Springer, 2006.
[20]
A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In POPL, pages 179–190. ACM Press, 1989.
[21]
V. Raman and H. Kress-Gazit. Explaining impossible high-level robot behaviors. IEEE Transactions on Robotics, 29(1):94–104, 2013.
[22]
F. Somenzi. CUDD: BDD package, University of Colorado, Boulder. http://vlsi. colorado.edu/~fabio/CUDD/cudd.pdf.
[23]
A. Walker and L. Ryzhyk. Predicate abstraction for reactive synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014, pages 219–226. IEEE, 2014.
[24]
T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. M. Murray. TuLiP: A Software Toolbox for Receding Horizon Temporal Logic Planning. In Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC ’11, pages 313–314, New York, NY, USA, 2011. ACM.

Cited By

View all
  • (2023)Adapting Specifications for Reactive Controllers2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)10.1109/SEAMS59076.2023.00012(1-12)Online publication date: May-2023
  • (2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
  • (2023)Which of My Assumptions are Unnecessary for Realizability and Why Should I Care?Proceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00030(221-232)Online publication date: 14-May-2023
  • Show More Cited By

Index Terms

  1. A symbolic justice violations transition system for unrealizable GR(1) specifications

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    ESEC/FSE 2017: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering
    August 2017
    1073 pages
    ISBN:9781450351058
    DOI:10.1145/3106237
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 21 August 2017

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. GR(1)
    2. reactive synthesis
    3. unrealizability

    Qualifiers

    • Research-article

    Funding Sources

    Conference

    ESEC/FSE'17
    Sponsor:

    Acceptance Rates

    Overall Acceptance Rate 112 of 543 submissions, 21%

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)6
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 07 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2023)Adapting Specifications for Reactive Controllers2023 IEEE/ACM 18th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)10.1109/SEAMS59076.2023.00012(1-12)Online publication date: May-2023
    • (2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
    • (2023)Which of My Assumptions are Unnecessary for Realizability and Why Should I Care?Proceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00030(221-232)Online publication date: 14-May-2023
    • (2022)Counterexample-guided inductive repair of reactive contractsProceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering10.1145/3524482.3527650(46-57)Online publication date: 18-May-2022
    • (2022)Dynamic update for synthesized GR(1) controllersProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510054(786-797)Online publication date: 21-May-2022
    • (2022)Probabilistic synthesis against GR(1) winning conditionFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-020-0076-z16:2Online publication date: 1-Apr-2022
    • (2021)Unrealizable Cores for Reactive Systems SpecificationsProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00016(25-36)Online publication date: 22-May-2021
    • (2021)Reactive synthesis with spectraProceedings of the 43rd International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion52605.2021.00136(320-321)Online publication date: 25-May-2021
    • (2021)Unrealizable cores for reactive systems specificationsProceedings of the 43rd International Conference on Software Engineering: Companion Proceedings10.1109/ICSE-Companion52605.2021.00097(217-218)Online publication date: 25-May-2021
    • (2020)Minimal Assumptions Refinement for Realizable SpecificationsProceedings of the 8th International Conference on Formal Methods in Software Engineering10.1145/3372020.3391557(66-76)Online publication date: 7-Oct-2020
    • Show More Cited By

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Media

    Figures

    Other

    Tables

    Share

    Share

    Share this Publication link

    Share on social media