Complexity results in revising UNITY programs

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: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Journal of the ACM (JACM), v.43 n.1, p.116-146, Jan. 1996 [doi>10.1145/227595.227602]
• 3: Eugene Asarin , Oded Maler, As Soon as Possible: Time Optimal Control for Timed Automata, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.19-30, March 29-31, 1999
• 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: Paul C. Attie , E. Allen Emerson, Synthesis of concurrent programs for an atomic read/write model of computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.2, p.187-242, March 2001 [doi>10.1145/383043.383044]
• 6: Paul C. Attie, Synthesis of Large Concurrent Programs via Pairwise Composition, Proceedings of the 10th International Conference on Concurrency Theory, p.130-145, August 24-27, 1999
• 7: Paul C. Attie , Anish Arora , E. Allen Emerson, Synthesis of fault-tolerant concurrent programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.1, p.125-185, January 2004 [doi>10.1145/963778.963782]
• 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: Borzoo Bonakdarpour , Sandeep S. Kulkarni, Exploiting Symbolic Techniques in Automated Synthesis of Distributed Programs with Large State Space, Proceedings of the 27th International Conference on Distributed Computing Systems, p.3, June 25-27, 2007 [doi>10.1109/ICDCS.2007.109]
• 12: Borzoo Bonakdarpour , Sandeep S. Kulkarni, SYCRAFT: A Tool for Synthesizing Distributed Fault-Tolerant Programs, Proceedings of the 19th international conference on Concurrency Theory, August 19-22, 2008, Toronto, Canada [doi>10.1007/978-3-540-85361-9_16]
• 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: Al Carruth, Real-Time Unity, University of Texas at Austin, Austin, TX, 1994
• 15: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 16: Costas Courcoubetis, Minimum and Maximum Delay Problems in Real-Time Systems, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.399-409, July 01-04, 1991
• 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: Edsger W. Dijkstra, Self-stabilizing systems in spite of distributed control, Communications of the ACM, v.17 n.11, p.643-644, Nov. 1974 [doi>10.1145/361179.361202]
• 19: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 20: Deepak D'Souza , P. Madhusudan, Timed Control Synthesis for External Specifications, Proceedings of the 19th Annual Symposium on Theoretical Aspects of Computer Science, p.571-582, March 14-16, 2002
• 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: David Eppstein, Finding the k Shortest Paths, SIAM Journal on Computing, v.28 n.2, p.652-673, April 1999 [doi>10.1137/S0097539795290477]
• 24: Marco Faella , Salvatore La Torre , Aniello Murano, Dense Real-Time Games, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.167-176, July 22-25, 2002
• 25: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 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: Sandeep S. Kulkarni , Ali Ebnenasir, The Complexity of Adding Failsafe Fault-Tolerance, Proceedings of the 22 nd International Conference on Distributed Computing Systems (ICDCS'02), p.337, July 02-05, 2002
• 31: Sandeep S. Kulkarni , Ali Ebnenasir, Enhancing The Fault-Tolerance of Nonmasking Programs, Proceedings of the 23rd International Conference on Distributed Computing Systems, p.441, May 19-22, 2003
• 32: Sandeep S. Kulkarni , Ali Ebnenasir, Automated Synthesis of Multitolerance, Proceedings of the 2004 International Conference on Dependable Systems and Networks, p.209, June 28-July 01, 2004
• 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: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 37: D. Paik , S. Reddy , S. Sahni, Deleting Vertices to Bound Path Length, IEEE Transactions on Computers, v.43 n.9, p.1091-1096, September 1994 [doi>10.1109/12.312117]
• 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: A. Pnueli , R. Rosner, On the synthesis of a reactive module, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.179-190, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75293]
• 40: Amir Pnueli , Roni Rosner, On the Synthesis of an Asynchronous Reactive Module, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.652-671, July 11-15, 1989
• 41: Ramadge, P. and Wonham, W. 1989. The control of discrete event systems. Proc. IEEE 77, 1, 81--98.
• 42: Kurt Ryan Rohloff , Stephane Lafortune, Computations on distributed discrete-event systems, University of Michigan, Ann Arbor, MI, 2004
• 43: Rudie, K., Lafortune, S., and Lin, F. 2003. Minimal communication in a distributed discrete-event systems. IEEE Trans. Autom. Control 48, 6.
• 44: Wolfgang Thomas, Infinite Games and Verification (Extended Abstract of a Tutorial), Proceedings of the 14th International Conference on Computer Aided Verification, p.58-64, July 27-31, 2002
• 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.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.3 Tradeoffs among Complexity Measures

General Terms:
Algorithms, Theory, Verification

Keywords:
UNITY, formal methods