PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements

Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Konferencja
International Workshop on CONCURRENCY, SPECIFICATION, and PROGRAMMING (CS&P 2015), (24; 28-30.09.2015, Rzeszów, Poland).
Języki publikacji
EN
Abstrakty
EN
For many program analysis problems it is useful to have means to efficiently prove that given programs have similar (equivalent) behaviors. Unfortunately, in most cases to prove the behavioral equivalence is an undecidable problem. A common way to overcome such undecidability is to consider a model of programs with an abstract semantics based on the real one, in which only some simple properties are captured, and to provide an efficient equivalence-checking algorithm for the model. We focus on two kinds of properties of data-modifying statements of imperative programs. Statements a and b are commutative, if the execution of sequences ab and ba lead to the same result. A statement b is (left-)absorptive for a statement a, if the execution of sequences ab and b lead to the same result. We consider propositional program models in which commutativity and absorption properties are caprtured (CA-models). Formally, data states for a CA-model are elements of a monoid over the set of statement symbols, defined by an arbitrary set of relations of the form ab = ba (for commutativity) and ab = b (for absorption). We propose an equivalence-checking algorithm for CA-models based on (what we call) progressive monoids. The algorithm terminates in time polynomial in size of programs. As a consequence, we prove a polynomial-time decidability for the equivalence problem in such CA-models.
Wydawca
Rocznik
Strony
315--336
Opis fizyczny
Bibliogr. 17 poz., rys.
Twórcy
autor
  • National Research University Higher School of Economics, 3 Kochnovsky Proezd, 125319 Moscow, Russia
Bibliografia
  • [1] Rice Hd. Classes of Recursively Enumerable Sets and Their Decision Problems. Transactions of the American Mathematical Society. 1953;74(2):358–366. Available from: http://www.jstor.org/stable/1990888.
  • [2] Aho AV, Lam MS, Sethi R, Ullman JD. Compilers: Principles, Techniques, and Tools (2nd Edition). Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc.; 2006. ISBN-13: 978-0321486813, 10: 0321486811.
  • [3] Zakharov V. An efficient and unified approach to the decidability of equivalence of propositional programs. In: Larsen K, Skyum S, Winskel G, editors. Automata, Languages and Programming. vol. 1443 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 1998. p. 247–258. doi:10.1007/BFb0055058.
  • [4] Zakharov VA. Program equivalence checking by two-tape automata. Cybernetics and Systems Analysis. 2010;46(4):554–562. doi:10.1007/s10559-010-9232-z.
  • [5] Harel D, Tiuryn J, Kozen D. Dynamic Logic. Cambridge, MA, USA: MIT Press; 2000. ISBN-0262082896.
  • [6] Hunt HB, Constable RL, Sahni S. On the Computational Complexity of Program Scheme Equivalence. SIAM Journal on Computing. 1980;9(2):396–416. doi:10.1137/0209031.
  • [7] Rutledge JD. On Ianov’s Program Schemata. Journal of the ACM. 1964;11(1):1–9. doi:10.1145/321203.321204.
  • [8] Hopcroft JE, Motwani R, Ullman JD. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc.; 2006. ISBN-13:978-0321455369, 10:0321455363.
  • [9] Kozen D. Kleene Algebra with Tests and Commutativity Conditions. Ithaca, NY, USA; 1996. doi:10.1007/3-540-61042-1_35.
  • [10] Zakharov VA. On the Decidability of the Equivalence Problem for Monadic Recursive Programs. Theoretical Informatics and Applications. 2000;34(2):157–172. doi:10.1051/ita:2000112.
  • [11] Glushkov VM, Letichevskii AA. Theory of Algorithms and Discrete Processors. In: Tou J, editor. Advances in Information Systems Science. Springer US; 1969. p. 1–58. doi:10.1007/978-1-4615-9050-7_1.
  • [12] Böhm S, Göller S, Jancar P. Equivalence of Deterministic One-counter Automata is NL-complete. In: Proceedings of the Forty-fifth Annual ACM Symposium on Theory of Computing. STOC ’13. New York, NY, USA: ACM; 2013. p. 131–140. doi:10.1145/2488608.2488626.
  • [13] Debski W, Fraczak W. Concatenation State Machines and Simple Functions. In: Domaratzki M, Okhotin A, Salomaa K, Yu S, editors. Implementation and Application of Automata. vol. 3317 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2005. p. 113–124. doi:10.1007/978-3-540-30500-2_11.
  • [14] Bastien C, Czyzowicz J, Fraczak W, Rytter W. Prime Normal Form and Equivalence of Simple Grammars. In: Farr J, Litovsky I, Schmitz S, editors. Implementation and Application of Automata. vol. 3845 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2006. p. 78–89. doi:10.1016/j.tcs.2006.07.021.
  • [15] Harju T, Karhumäki J. The equivalence problem of multitape finite automata. Theoretical Computer Science. 1991;78(2):347–355. doi:10.1016/0304-3975(91)90356-7.
  • [16] de Souza R. On the Decidability of the Equivalence for k-Valued Transducers. In: Ito M, Toyama M, editors. Developments in Language Theory. vol. 5257 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2008. p. 252–263. doi:10.1007/978-3-540-85780-8_20.
  • [17] Podymov VV, Zakharov VA. On a semigroup model of sequential programs specified by means of two-tape automata. Belgorod State University Scientific Bulletin History Political science Economics Information technologies. 2010;7(78)(14/1):94–101.
Uwagi
Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-c6131131-3b48-4bf5-bcb7-82e94f45b380
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.