research-article

Towards Efficient Implementation of Realizability Checking for Reactive System Specifications

Authors:

Masaya Shimakawa,

Shohei Mochizuki,

Takashi Tomita,

Shigeki Hagihara,

Naoki YonezakiAuthors Info & Claims

ICSCA '19: Proceedings of the 2019 8th International Conference on Software and Computer Applications

Pages 347 - 352

https://doi.org/10.1145/3316615.3316634

Published: 19 February 2019 Publication History

Abstract

Realizability checking is used to detect flaws in reactive system specifications that are difficult for humans to find. However, these checks are computationally costly. To address this problem, researchers have studied efficient methods for implementing such checking procedures. In this paper, we propose a new implementation method of realizability checking. While symbolic approaches have been adopted in many previous methods, we take a partially symbolic approach, in which binary decision diagrams (BDDs) are used partially. We developed a prototype realizability checker based on our method, and experimentally compared it to tools based on other implementation methods. Our prototype was efficient in comparison to the other tools.

References

[1]

Abadi, M., Lamport, L. and Wolper, P. Realizable and unrealizable specifications of reactive systems. In Proc. 16th International Colloquium on Automata, Languages, and Programming, volume 372 of LNCS, pages 1--17. Springer, 1989.

Digital Library

[2]

Aoshima, T., Sakuma, K. and Yonezaki, N. An efficient verification procedure supporting evolution of reactive system specifications. In Proc. International Workshop on Principles of Software Evolution, IWPSE 2001, pages 182--185, 2001.

Digital Library

[3]

Babiak, T., Křetínský, M., Řehák, V. and Strejček, J. LTL to Büchi automata translation: Fast and more deterministic. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of LNCS, pages 95--109. Springer, 2012.

Digital Library

[4]

Bohy, A., Bruyère, V., Filiot, E., Jin, N. and Raskin, J, -F. Acacia+, a tool for LTL synthesis. In Proc. 24th International Conference on Computer Aided Verification, volume 7358 of LNCS, pages 652--657. Springer, 2012.

Digital Library

[5]

Ehlers, R. Symbolic bounded synthesis. In Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pages 365--379. Springer, 2010.

Digital Library

[6]

Ehlers, R. Unbeast: Symbolic bounded synthesis. In Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 6605 of LNCS, pages 272--275. Springer, 2011.

Digital Library

[7]

Ehlers, R. ACTL ∩ LTL synthesis. In Proc. 24th International Conference on Computer Aided Verification, volume 7358 of LNCS, pages 39--54. Springer, 2012.

Digital Library

[8]

Filiot, E., Jin, N. and Raskin, J, -F. An antichain algorithm for LTL realizability. In Proc. 21st International Conference on Computer Aided Verification, volume 5643 of LNCS, pages 263--277. Springer, 2009.

Digital Library

[9]

Filiot, E., Jin, N. and Raskin, J, -F. Compositional algorithms for LTL synthesis. In Proc. 8th International Conference on Automated Technology for Verification and Analysis, volume 6252 of LNCS, pages 112--127. Springer, 2010.

Digital Library

[10]

Hagihara, S., Egawa, N., Shimakawa, M. and Yonezaki, N. Minimal strongly unsatisfiable subsets of reactive system specifications. In Proc. 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pages 629--634. ACM, 2014.

Digital Library

[11]

Hagihara, S., Ueno, A., Tomita, T., Shimakawa, M. and Yonezaki, N. Simple synthesis of reactive systems with tolerance for unexpected environmental behavior. In Proc. 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE '16, pages 15--21. ACM, 2016.

Digital Library

[12]

Ito, S., Ichinose, T., Shimakawa, M., Izumi, N., Hagihara, S. and Yonezaki, N. Qualitative analysis of gene regulatory networks by temporal logic. Theoretical Computer Science, 594:151--179, 2015.

Digital Library

[13]

Jobstmann, B. and Bloem, R. Optimizations for LTL synthesis. In Proc. Formal Methods in Computer Aided Design, FMCAD 2006, pages 117--124. IEEE Computer Society, 2006.

Digital Library

[14]

Kupferman, O. and Vardi, M. Y. Safraless decision procedures. In Proc. 46th Annual IEEE Symposium on Foundations of Computer Science, pages 531--542. IEEE Computer Society, 2005.

Digital Library

[15]

Maidi, M. The common fragment of CTL and LTL. In Proc. 41st Annual Symposium on Foundations of Computer Science, pages 643--652. IEEE Computer Society, 2000.

Digital Library

[16]

Mochizuki, S., Shimakawa, M., Hagihara, S. and Yonezaki, N. Fast translation from LTL to Büchi automata via non-transition-based automata. In Proc. 16th International Conference on Formal Engineering Methods, ICFEM 2014, volume 8829 of LNCS, pages 364--379. Springer, 2014.

[17]

Pnueli, A. and Rosner, R. On the synthesis of a reactive module. In Proc. 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989, pages 179--190. ACM, 1989.

Digital Library

[18]

Schewe, S. and Finkbeiner, B. Bounded synthesis. In Proc. 5th International Symposium Automated Technology Verification and Analysis, volume 4762 of LNCS, pages 474--488. Springer, 2007.

Digital Library

[19]

Shimakawa, M., Hagihara, S. and Yonezaki, N. Complexity of checking strong satisfiability of reactive system specifications. In Proc. International Joint Conference on Advances in Signal Processing and Information Technology, SPIT 2012, pages 42--51, 2012.

[20]

Shimakawa, M., Hagihara, S. and Yonezaki, N. Complexity of strong satisfiability problems for reactive system IEICE Trans. Inf. & Syst., E96-D(10):2187--2193, 2013.

[21]

Shimakawa, M., Hagihara, S. and Yonezaki, N. SAT-based bounded strong satisfiability checking of reactive system specifications. In Proc. International Conference on Information and Communication Technology, ICT-EurAsia 2013, volume 7804 of LNCS, pages 60--70. Springer, 2013.

Digital Library

[22]

Shimakawa, M., Hagihara, S. and Yonezaki, N. Bounded strong satisfiability checking of reactive system specifications. IEICE Trans. Inf. & Syst., E97-D(7):1746--1755, 2014.

[23]

Shimakawa, M., Hagihara, S. and Yonezaki, N. Reducing bounded realizability analysis to reachability checking. In Proc. 9th International Workshop on Reachability Problems, volume 9328 of LNCS, pages 140--152. Springer, 2015.

[24]

Shimakawa, M., Osari, K., Hagihara, S. and Yonezaki, N. Modularization of formal specifications or efficient synthesis of reactive systems. In Proc. 6th International Conference on Software and Computer Applications, ICSCA 2017, pages 208--213. ACM, 2017.

Digital Library

[25]

Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S. and Yonezaki, N. Safraless LTL synthesis considering maximal realizability. Acta Informatica, 54(7):655--692, 2017.

Digital Library

Cited By

Shimakawa MHayashi KHagihara SYonezaki N(2020)Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal LogicProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384572(17-20)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384572

Index Terms

Towards Efficient Implementation of Realizability Checking for Reactive System Specifications
1. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
A formal approach for the development of reactive systems

Context: This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA^+ to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

ICSCA '19: Proceedings of the 2019 8th International Conference on Software and Computer Applications

February 2019

611 pages

ISBN:9781450365734

DOI:10.1145/3316615

Copyright © 2019 ACM.

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]

In-Cooperation

University of New Brunswick: University of New Brunswick

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 February 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

ICSCA '19

ICSCA '19: 2019 8th International Conference on Software and Computer Applications

February 19 - 21, 2019

Penang, Malaysia

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
38
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shimakawa MHayashi KHagihara SYonezaki N(2020)Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal LogicProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384572(17-20)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384572

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents