research-article

Complexity results in revising UNITY programs

Authors:

Borzoo Bonakdarpour,

Sandeep S. KulkarniAuthors Info & Claims

ACM Transactions on Autonomous and Adaptive Systems (TAAS), Volume 4, Issue 1

Article No.: 5, Pages 1 - 28

https://doi.org/10.1145/1462187.1462192

Published: 09 February 2009 Publication History

Abstract

We concentrate on automatic revision of untimed and real-time programs with respect to UNITY properties. The main focus of this article is to identify instances where addition of UNITY properties can be achieved efficiently (in polynomial time) and where the problem of adding UNITY properties is difficult (NP-complete). Regarding efficient revision, we present a sound and complete algorithm that adds a single leads-to property (respectively, bounded-time leads-to property) and a conjunction of unless, stable, and invariant properties (respectively, bounded-time unless and stable) to an existing untimed (respectively, real-time) UNITY program in polynomial-time in the state space (respectively, region graph) of the given program. Regarding hardness results, we show that (1) while one leads-to (respectively, ensures) property can be added in polynomial-time, the problem of adding two such properties (or any combination of leads-to and ensures) is NP-complete, (2) if maximum non-determinism is desired then the problem of adding even a single leads-to property is NP-complete, and (3) the problem of providing maximum non-determinism while adding a single bounded-time leads-to property to a real-time program is NP-complete (in the size of the program's region graph) even if the original program satisfies the corresponding unbounded leads-to property.

References

[1]

Alur, R. and Dill, D. 1994. A theory of timed automata. Theor. Comput. Sci. 126, 2, 183--235.

Digital Library

[2]

Alur, R., Feder, T., and Henzinger, T. 1996. The benefits of relaxing punctuality. J. ACM 43, 1, 116--146.

Digital Library

[3]

Asarin, E. and Maler, O. 1999. As soon as possible: Time optimal control for timed automata. In Proceedings of the Conference on Hybrid Systems: Computation and Control (HSCC). 19--30.

Digital Library

[4]

Asarin, E., Maler, O., Pnueli, A., and Sifakis, J. 1998. Controller synthesis for timed automata. In Proceedings of the IFAC Symposium on System Structure and Control. 469--474.

[5]

Attie, P. and Emerson, E. A. 2001. Synthesis of concurrent programs for an atomic read/write model of computation. ACM Trans. Prog. Lang. Syst. 23, 2, 187--242.

Digital Library

[6]

Attie, P. C. 1999. Synthesis of large concurrent programs via pairwise composition. In Proceedings of the International Conference on Concurrency Theory (CONCUR). Springer-Verlag, 130--145.

Digital Library

[7]

Attie, P. C., Arora, A., and Emerson, E. A. 2004. Synthesis of fault-tolerant concurrent programs. ACM Trans. Prog. Lang. Syst. 26, 1, 125--185.

Digital Library

[8]

Bang-Jensen, J. and Gutin, G. 2002. Digraphs: Theory, Algorithms and Applications. Springer.

[9]

Bonakdarpour, B. and Kulkarni, S. S. 2006a. Automated incremental synthesis of timed automata. In Proceedings of the International Workshop on Formal Methods for Industrial Critical Systems (FMICS). Lecture Notes in Computer Science, vol. 4346, 261--276.

[10]

Bonakdarpour, B. and Kulkarni, S. S. 2006b. Incremental synthesis of fault-tolerant real-time programs. In Proceedings of the International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS). Lecture Notes in Computer Science, vol. 4280, 122--136.

[11]

Bonakdarpour, B. and Kulkarni, S. S. 2007. Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In Proceedings of the IEEE International Conference on Distributed Computing Systems (ICDCS). 3--10.

Digital Library

[12]

Bonakdarpour, B. and Kulkarni, S. S. 2008. SYCRAFT: A tool for synthesizing fault-tolerant distributed programs. In Proceedings of the International Conference on Concurrency Theory (CONCUR). 167--171.

Digital Library

[13]

Bouyer, P., D'Souza, D., Madhusudan, P., and Petit, A. 2003. Timed control with partial observability. In Proceedings of the International Conference on Computer Aided Verification (CAV). 180--192.

[14]

Carruth, A. 1994. Real-time UNITY. Tech. rep. CS-TR-94-10, University of Texas at Austin.

Digital Library

[15]

Chandy, K. M. and Misra, J. 1988. Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc., Boston, MA.

Digital Library

[16]

Courcoubetis, C. and Yannakakis, M. 1991. Minimum and maximum delay problems in real-time systems. In Proceedings of the International Conference on Computer-Aided Verificaion (CAV). 399--409.

Digital Library

[17]

de Alfaro, L., Faella, M., Henzinger, T. A., Majumdar, R., and Stoelinga, M. 2003. The element of surprise in timed games. In Proceedings of the International Conference on Concurrency Theory (CONCUR).

[18]

Dijkstra, E. W. 1974. Self-stabilizing systems in spite of distributed control. Comm. ACM 17, 11.

Digital Library

[19]

Dijkstra, E. W. 1990. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.

Digital Library

[20]

D'Souza, D. and Madhusudan, P. 2002. Timed control synthesis for external specifications. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS). 571--582.

Digital Library

[21]

Ebnenasir, A., Kulkarni, S. S., and Bonakdarpour, B. 2005. Revising UNITY programs: Possibilities and limitations. In Proceedings of the Conference on Principles of Distributed Systems (OPODIS). 275--290.

[22]

Emerson, E. A. and Clarke, E. M. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Prog. 2, 3, 241--266.

[23]

Eppstein, D. 1999. Finding the k shortest paths. SIAM J. Comput. 28, 2, 652--673.

Digital Library

[24]

Faella, M., LaTorre, S., and Murano, A. 2002. Dense real-time games. In Logic in Computer Science (LICS). 167--176.

Digital Library

[25]

Holzmann, G. 1997. The model checker spin. IEEE Trans. Software Engin.

Digital Library

[26]

Jobstmann, B., Griesmayer, A., and Bloem, R. 2005. Program repair as a game. In Proceedings of the Conference on Computer Aided Verification (CAV). 226--238.

[27]

Karp, R. M. 1972. Reducibility among combinatorial problems. In Proceedings of the Symposium on Complexity of Computer Computations. 85--103.

[28]

Kulkarni, S. S., Arora, A., and Chippada, A. 2001. Polynomial time synthesis of Byzantine agreement. In Proceedings of the Symposium on Reliable Distributed Systems (SRDS). 130--140.

[29]

Kulkarni, S. S., Arora, A., and Ebnenasir, A. 2007. Software Engineering and Fault-Tolerance. World Scientific Publishing Co. Pte. Ltd (Chapter: Adding Fault-Tolerance to State Machine-Based Designs).

[30]

Kulkarni, S. S. and Ebnenasir, A. 2002. The complexity of adding failsafe fault-tolerance. In Proceedings of the International Conference on Distributed Computing Systems (ICDCS). 337--344.

Digital Library

[31]

Kulkarni, S. S. and Ebnenasir, A. 2003. Enhancing the fault-tolerance of nonmasking programs. In Proceedings of the International Conference on Distributed Computing Systems (ICDCS).

Digital Library

[32]

Kulkarni, S. S. and Ebnenasir, A. 2004. Automated synthesis of multitolerance. In Proceedings of the International Conference on Dependable Systems and Networks (DSN). 209--219.

Digital Library

[33]

Lafortune, S. and Lin, F. 1992. On tolerable and desirable behaviors in supervisory control of discrete event systems. Discr. Event Dynam. Syst. 1, 1, 61--92.

[34]

Lin, F. and Wonham, W. M. 1990. Decentralized control and coordination of discrete-event systems with partial observation. IEEE Trans. Autom. Control 35, 12.

[35]

Maler, O., Nickovic, D., and Pnueli, A. 2006. From MITL to timed automata. In Proceedings of the Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). 274--289.

[36]

Manna, Z. and Wolper, P. 1984. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Prog. Lang. Syst. 6, 1, 68--93.

Digital Library

[37]

Paik, D., Reddy, S., and Sahni, S. 1994. Deleting vertices to bound path length. IEEE Trans. Comput. 43, 9, 1091--1096.

Digital Library

[38]

Paik, D., Reddy, S. M., and Sahni, S. 1998. Vertex splitting in dags and applications to partial scan designs and lossy circuits. Int. J. Found. Comput. Sci. 9, 4, 377--398.

[39]

Pnueli, A. and Rosner, R. 1989a. On the synthesis of a reactive module. In Proceedings of the Conference on Principles of Programming Languages (POPL). 179--190.

Digital Library

[40]

Pnueli, A. and Rosner, R. 1989b. On the synthesis of an asynchronous reactive module. In Proceedings of the International Colloqium on Automata, Languages, and Programming (ICALP). 652--671.

Digital Library

[41]

Ramadge, P. and Wonham, W. 1989. The control of discrete event systems. Proc. IEEE 77, 1, 81--98.

[42]

Rohloff, K. R. 2004. Computations on distributed discrete-event systems. Ph.D. thesis, University of Michigan.

Digital Library

[43]

Rudie, K., Lafortune, S., and Lin, F. 2003. Minimal communication in a distributed discrete-event systems. IEEE Trans. Autom. Control 48, 6.

[44]

Thomas, W. 2002. Infinite games and verification (extended abstract of a tutorial). In Proceedings of the International Conference on Computer Aided Verification (CAV). 58--64.

Digital Library

[45]

Wallmeier, N., Hütten, P., and Thomas, W. 2003. Symbolic synthesis of finite-state controllers for request-response specifications. In Proceedings of the Conference on Implementation and Application of Automata (CIAA). 11--22.

Cited By

Bonakdarpour BFinkbeiner B(2020)Controller Synthesis for Hyperproperties2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00033(366-379)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00033
Roohitavaf MKulkarni S(2019)Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions †Future Internet10.3390/fi1107014411:7(144)Online publication date: 4-Jul-2019
https://doi.org/10.3390/fi11070144
Bonakdarpour BFinkbeiner B(2019)Program Repair for HyperpropertiesAutomated Technology for Verification and Analysis10.1007/978-3-030-31784-3_25(423-441)Online publication date: 28-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31784-3_25
Show More Cited By

Index Terms

Complexity results in revising UNITY programs

Recommendations

Revising UNITY programs: possibilities and limitations
OPODIS'05: Proceedings of the 9th international conference on Principles of Distributed Systems

We concentrate on automatic addition of UNITY properties unless, stable, invariant, and leads-to to programs. We formally define the problem of adding UNITY properties to programs while preserving their existing properties. For cases where one ...
Revising Distributed UNITY Programs Is NP-Complete
OPODIS '08: Proceedings of the 12th International Conference on Principles of Distributed Systems

We focus on automated revision techniques for adding Unity properties to distributed programs. We show that unlike centralized programs, where multiple safety properties along with one progress property can be simultaneously added in polynomial-time, ...
Deducing fairness properties in UNITY logic—a new completeness result

We explore the use of UNITY logic in specifying and verifying fairness properties of UNITY and UNITY-like programs whose semantics can be modeled by weakly fair transition systems. For such programs, strong fairness properties in the form of “if p holds ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Autonomous and Adaptive Systems

ACM Transactions on Autonomous and Adaptive Systems Volume 4, Issue 1

January 2009

213 pages

ISSN:1556-4665

EISSN:1556-4703

DOI:10.1145/1462187

Issue’s Table of Contents

Copyright © 2009 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 February 2009

Accepted: 01 September 2008

Revised: 01 July 2008

Received: 01 March 2007

Published in TAAS Volume 4, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
364
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bonakdarpour BFinkbeiner B(2020)Controller Synthesis for Hyperproperties2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00033(366-379)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00033
Roohitavaf MKulkarni S(2019)Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions †Future Internet10.3390/fi1107014411:7(144)Online publication date: 4-Jul-2019
https://doi.org/10.3390/fi11070144
Bonakdarpour BFinkbeiner B(2019)Program Repair for HyperpropertiesAutomated Technology for Verification and Analysis10.1007/978-3-030-31784-3_25(423-441)Online publication date: 28-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31784-3_25
Roohitavaf MKulkarni S(2016)Stabilization and fault-tolerance in presence of unchangeable environment actionsProceedings of the 17th International Conference on Distributed Computing and Networking10.1145/2833312.2833324(1-10)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2833312.2833324
Roohitavaf MLin YKulkarni S(2016)Lazy Repair for Addition of Fault-Tolerance to Distributed Programs2016 IEEE International Parallel and Distributed Processing Symposium (IPDPS)10.1109/IPDPS.2016.78(1071-1080)Online publication date: May-2016
https://doi.org/10.1109/IPDPS.2016.78
Roohitavaf MKulkarni S(2016)Automatic Addition of Conflicting PropertiesStabilization, Safety, and Security of Distributed Systems10.1007/978-3-319-49259-9_25(310-326)Online publication date: 3-Nov-2016
https://doi.org/10.1007/978-3-319-49259-9_25
Essen CJobstmann B(2015)Program repair without regretFormal Methods in System Design10.1007/s10703-015-0223-647:1(26-50)Online publication date: 1-Aug-2015
https://dl.acm.org/doi/10.1007/s10703-015-0223-6
Abujarad FLin YBonakdarpour BKulkarni S(2015)The complexity of automated addition of fault-tolerance without explicit legitimate statesDistributed Computing10.1007/s00446-014-0227-228:3(201-219)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1007/s00446-014-0227-2
Bonakdarpour BKulkarni S(2015)Synthesizing bounded-time 2-phase fault recoveryFormal Aspects of Computing10.1007/s00165-014-0325-827:1(1-31)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1007/s00165-014-0325-8
Ebnenasir A(2015)Incremental Realization of Safety Requirements: Non-determinism vs. ModularityFundamentals of Software Engineering10.1007/978-3-319-24644-4_11(159-175)Online publication date: 12-Nov-2015
https://doi.org/10.1007/978-3-319-24644-4_11
Show More Cited By

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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents