Unguardedness mostly means many solutions

A widely accepted method to specify (possibly infinite) behaviour is to define it as the solution, in some process algebra, of a recursive specification, i.e., a system of recursive equations over the fundamental operations of the process algebra. The method only works if the recursive specification...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2011-06, Vol.412 (28), p.3090-3100
Main Authors: Baeten, Jos C.M., Luttik, Bas
Format: Article
Language:English
Subjects:
Algebra
Algorithmics. Computability. Computer arithmetics
Applied sciences
Computer science
control theory
systems
Computer simulation
Exact sciences and technology
Mathematical analysis
Mathematical models
Mathematics
Miscellaneous
Nonlinear algebraic and transcendental equations
Numerical analysis
Numerical analysis. Scientific computation
Process algebra
Recursive
Recursive specification
Sciences and techniques of general use
Software
Software engineering
Specifications
Theorems
Theoretical computing
Unguarded equation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A widely accepted method to specify (possibly infinite) behaviour is to define it as the solution, in some process algebra, of a recursive specification, i.e., a system of recursive equations over the fundamental operations of the process algebra. The method only works if the recursive specification has a unique solution in the process algebra; it is well-known that guardedness is a sufficient requirement on a recursive specification to guarantee a unique solution in any of the standard process algebras. In this paper we investigate to what extent guardedness is also a necessary requirement to ensure unique solutions. We prove a theorem to the effect that all unguarded recursive specifications over BPA have infinitely many solutions in the standard models for BPA . In contrast, we observe that there exist recursive specifications over PA , necessarily involving parallel composition, that have a unique solution, or finitely many solutions in the standard models for PA .
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2011.02.046