Behavioral rewrite systems and behavioral productivity

Grigore Roşu, Dorel Lucanu

Research output: Contribution to journalArticlepeer-review


This paper introduces behavioral rewrite systems, where rewriting is used to evaluate experiments, and behavioral productivity, which says that each experiment can be fully evaluated, and investigates some of their properties. First, it is shown that, in the case of (infinite) streams, behavioral productivity generalizes and may bring to a more basic rewriting setting the existing notion of stream productivity defined in the context of infinite rewriting and lazy strategies; some arguments are given that in some cases one may prefer the behavioral approach. Second, a behavioral productivity criterion is given, which reduces the problem to conventional term rewrite system termination, so that one can use off-the-shelf termination tools and techniques for checking behavioral productivity in general, not only for streams. Finally, behavioral productivity is shown to be equivalent to a proof-theoretic (rather than model-theoretic) notion of behavioral well-specifiedness, and its difficulty in the arithmetic hierarchy is shown to be-complete. All new concepts are exemplified over streams, infinite binary trees, and processes.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Behavioral rewrite systems and behavioral productivity'. Together they form a unique fingerprint.

Cite this