• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

An Afficient Equivalence-Checking Algorithm for a Model of Programs with Commutative and Absorptive Statements

P. 85-96.
Vladislav Podymov.

We present an efficient equivalence-checking algorithm for a propositional model of programs with semantics based on (what we call) progressive monoids on the finite set of statements generated by relations of a specific form. We consider arbitrary set of relations for commutativity (relations of the form ab=ba for statements a, b) and left absorption (relations of the form ab=b for statements a, b) properties. The main results are a polynomial-time decidability for the equivalence problem in the considered case, and an explicit description of an equivalence-checking algorithm which terminates in time polynomial in size of programs.

In book

Edited by: S. Zbigniew, L. Czaja. Vol. 1492: Proceedings of the 24th International Workshop on Concurrency, Specification and Programming. Rzeszow, Poland, September 28-30, 2015.. CEUR Workshop Proceedings, 2015.