Abstract
Existing algorithms for the automated model revision incur an impediment that the designers have to identify the legitimate states of original model. Experience suggests that of the inputs required for model revision, identifying such legitimate states is the most difficult. In this paper, we consider the problem of automated model revision without explicit legitimate states. We note that without the explicit legitimate states, in some instances, the complexity of model revision increases substantially (from P to NP-hard). In spite of this, we find that this formulation is relatively complete, i.e., if it was possible to perform model revision with explicit legitimate states then it is also possible to do so without the explicit identification of the legitimate states. Finally, we show if the problem of model revision can be solved with explicit legitimate states then the increased cost of solving it without explicit legitimate states is very small.
In summary, the results in this paper identify instances of model revision where the explicit knowledge of legitimate state is beneficial and where it is not very crucial.
This work was partially sponsored by the Air Force ContractFA9550-10-1-0178 NSF CNS 0914913.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abujarad, F., Kulkarni, S.S.: Complexity issues in automated model revision without explicit legitimate state. Technical Report MSU-CSE-10-19, Computer Science and Engineering, Michigan State University, East Lansing, Michigan (July 2010), Available as Technical Report MSU-CSE-10-19 at, http://www.cse.msu.edu/cgi-user/web/tech/reports?Year=2010
Abujarad, F., Kulkarni, S.S.: Weakest Invariant Generation for Automated Addition of Fault-Tolerance. Electronic Notes in Theoretical Computer Science 258(2), 3–15 (2009), Available as Technical Report MSU-CSE-09-29 at, http://www.cse.msu.edu/cgi-user/web/tech/reports?Year=2009
Arora, A., Gouda, M.G.: Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering 19(11), 1015–1027 (1993)
Asarin, E., Maler, O.: As soon as possible: Time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symposium on System Structure and Control, pp. 469–474 (1998)
Avižienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Transactions on Dependable and Secure Computing, 11–33 (2004)
Bonakdarpour, B., Kulkarni, S.S.: Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In: IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 3–10 (2007)
Bonakdarpour, B., Kulkarni, S.S.: Sycraft: A tool for synthesizing distributed fault-tolerant programs. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 167–171. Springer, Heidelberg (2008)
Bouyer, P., D’Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 180–192. Springer, Heidelberg (2003)
Faella, M., LaTorre, S., Murano, A.: Dense real-time games. In: Logic in Computer Science (LICS), pp. 167–176 (2002)
Gärtner, F.C., Jhumka, A.: Automating the addition of fail-safe fault-tolerance: Beyond fusion-closed specifications. In: FORMATS/FTRTFT, pp. 183–198 (2004)
Gartner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Computing Surveys (CSUR) 31(1), 1–26 (1999)
Kulkarni, S.S., Arora, A.: Automating the addition of fault-tolerance. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 82–93. Springer, Heidelberg (2000)
Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems 4(3), 382–401 (1982)
Mantel, H., Gärtner, F.C.: A case study in the mechanical verification of fault-tolerance. Technical Report TUD-BS-1999-08, Department of Computer Science, Darmstadt University of Technology (1999)
Somenzi, F.: CUDD: Colorado University Decision Diagram Package, http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abujarad, F., Kulkarni, S.S. (2010). Complexity Issues in Automated Model Revision without Explicit Legitimate State . In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2010. Lecture Notes in Computer Science, vol 6366. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16023-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-16023-3_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16022-6
Online ISBN: 978-3-642-16023-3
eBook Packages: Computer ScienceComputer Science (R0)