Loading…
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...
Saved in:
| Published in: | Theoretical computer science 2011-06, Vol.412 (28), p.3090-3100 |
|---|---|
| Main Authors: | , |
| Format: | Article |
| Language: | English |
| Subjects: | |
| 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!
|
| cited_by | cdi_FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63 |
|---|---|
| cites | cdi_FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63 |
| container_end_page | 3100 |
| container_issue | 28 |
| container_start_page | 3090 |
| container_title | Theoretical computer science |
| container_volume | 412 |
| creator | Baeten, Jos C.M. Luttik, Bas |
| description | 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
. |
| doi_str_mv | 10.1016/j.tcs.2011.02.046 |
| format | article |
| fullrecord | <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_907939076</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><els_id>S0304397511001940</els_id><sourcerecordid>907939076</sourcerecordid><originalsourceid>FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63</originalsourceid><addsrcrecordid>eNp9kE1LA0EMhgdRsFZ_gLdeRDzsmvnYzC6eRPyCghd7HqazszJlP-pkV-i_d0qLR3NICDzJm7yMXXPIOXC83-Sjo1wA5zmIHBSesBkvdZUJUalTNgMJKpOVLs7ZBdEGUhQaZ-xu1X9NNta-7j3RohtobHeLzts-NbbfLWhopzEMPV2ys8a25K-Odc5WL8-fT2_Z8uP1_elxmTkFYszU2iFKK0Gnu3RRY6MKWfq1TdqFxArWDSJHhT4BJYB1QtdeCg6okdco5-z2sHcbh-_J02i6QM63re39MJGpQFcypT3JD6SLA1H0jdnG0Nm4MxzM3hWzMckVs3fFgDDJlTRzc9xuydm2ibZ3gf4GhRKIJYjEPRw4n179CT4acsH3ztchejeaegj_qPwCGFh1GQ</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>907939076</pqid></control><display><type>article</type><title>Unguardedness mostly means many solutions</title><source>ScienceDirect Freedom Collection 2022-2024</source><creator>Baeten, Jos C.M. ; Luttik, Bas</creator><creatorcontrib>Baeten, Jos C.M. ; Luttik, Bas</creatorcontrib><description>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
.</description><identifier>ISSN: 0304-3975</identifier><identifier>EISSN: 1879-2294</identifier><identifier>DOI: 10.1016/j.tcs.2011.02.046</identifier><identifier>CODEN: TCSCDI</identifier><language>eng</language><publisher>Oxford: Elsevier B.V</publisher><subject>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</subject><ispartof>Theoretical computer science, 2011-06, Vol.412 (28), p.3090-3100</ispartof><rights>2011 Elsevier B.V.</rights><rights>2015 INIST-CNRS</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63</citedby><cites>FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&idt=24266802$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>Baeten, Jos C.M.</creatorcontrib><creatorcontrib>Luttik, Bas</creatorcontrib><title>Unguardedness mostly means many solutions</title><title>Theoretical computer science</title><description>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
.</description><subject>Algebra</subject><subject>Algorithmics. Computability. Computer arithmetics</subject><subject>Applied sciences</subject><subject>Computer science; control theory; systems</subject><subject>Computer simulation</subject><subject>Exact sciences and technology</subject><subject>Mathematical analysis</subject><subject>Mathematical models</subject><subject>Mathematics</subject><subject>Miscellaneous</subject><subject>Nonlinear algebraic and transcendental equations</subject><subject>Numerical analysis</subject><subject>Numerical analysis. Scientific computation</subject><subject>Process algebra</subject><subject>Recursive</subject><subject>Recursive specification</subject><subject>Sciences and techniques of general use</subject><subject>Software</subject><subject>Software engineering</subject><subject>Specifications</subject><subject>Theorems</subject><subject>Theoretical computing</subject><subject>Unguarded equation</subject><issn>0304-3975</issn><issn>1879-2294</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2011</creationdate><recordtype>article</recordtype><recordid>eNp9kE1LA0EMhgdRsFZ_gLdeRDzsmvnYzC6eRPyCghd7HqazszJlP-pkV-i_d0qLR3NICDzJm7yMXXPIOXC83-Sjo1wA5zmIHBSesBkvdZUJUalTNgMJKpOVLs7ZBdEGUhQaZ-xu1X9NNta-7j3RohtobHeLzts-NbbfLWhopzEMPV2ys8a25K-Odc5WL8-fT2_Z8uP1_elxmTkFYszU2iFKK0Gnu3RRY6MKWfq1TdqFxArWDSJHhT4BJYB1QtdeCg6okdco5-z2sHcbh-_J02i6QM63re39MJGpQFcypT3JD6SLA1H0jdnG0Nm4MxzM3hWzMckVs3fFgDDJlTRzc9xuydm2ibZ3gf4GhRKIJYjEPRw4n179CT4acsH3ztchejeaegj_qPwCGFh1GQ</recordid><startdate>20110620</startdate><enddate>20110620</enddate><creator>Baeten, Jos C.M.</creator><creator>Luttik, Bas</creator><general>Elsevier B.V</general><general>Elsevier</general><scope>6I.</scope><scope>AAFTH</scope><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>20110620</creationdate><title>Unguardedness mostly means many solutions</title><author>Baeten, Jos C.M. ; Luttik, Bas</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2011</creationdate><topic>Algebra</topic><topic>Algorithmics. Computability. Computer arithmetics</topic><topic>Applied sciences</topic><topic>Computer science; control theory; systems</topic><topic>Computer simulation</topic><topic>Exact sciences and technology</topic><topic>Mathematical analysis</topic><topic>Mathematical models</topic><topic>Mathematics</topic><topic>Miscellaneous</topic><topic>Nonlinear algebraic and transcendental equations</topic><topic>Numerical analysis</topic><topic>Numerical analysis. Scientific computation</topic><topic>Process algebra</topic><topic>Recursive</topic><topic>Recursive specification</topic><topic>Sciences and techniques of general use</topic><topic>Software</topic><topic>Software engineering</topic><topic>Specifications</topic><topic>Theorems</topic><topic>Theoretical computing</topic><topic>Unguarded equation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Baeten, Jos C.M.</creatorcontrib><creatorcontrib>Luttik, Bas</creatorcontrib><collection>ScienceDirect Open Access Titles</collection><collection>Elsevier:ScienceDirect:Open Access</collection><collection>Pascal-Francis</collection><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>Theoretical computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Baeten, Jos C.M.</au><au>Luttik, Bas</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Unguardedness mostly means many solutions</atitle><jtitle>Theoretical computer science</jtitle><date>2011-06-20</date><risdate>2011</risdate><volume>412</volume><issue>28</issue><spage>3090</spage><epage>3100</epage><pages>3090-3100</pages><issn>0304-3975</issn><eissn>1879-2294</eissn><coden>TCSCDI</coden><abstract>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
.</abstract><cop>Oxford</cop><pub>Elsevier B.V</pub><doi>10.1016/j.tcs.2011.02.046</doi><tpages>11</tpages><oa>free_for_read</oa></addata></record> |
| fulltext | fulltext |
| identifier | ISSN: 0304-3975 |
| ispartof | Theoretical computer science, 2011-06, Vol.412 (28), p.3090-3100 |
| issn | 0304-3975 1879-2294 |
| language | eng |
| recordid | cdi_proquest_miscellaneous_907939076 |
| source | ScienceDirect Freedom Collection 2022-2024 |
| 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 |
| title | Unguardedness mostly means many solutions |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-29T09%3A10%3A06IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Unguardedness%20mostly%20means%20many%20solutions&rft.jtitle=Theoretical%20computer%20science&rft.au=Baeten,%20Jos%20C.M.&rft.date=2011-06-20&rft.volume=412&rft.issue=28&rft.spage=3090&rft.epage=3100&rft.pages=3090-3100&rft.issn=0304-3975&rft.eissn=1879-2294&rft.coden=TCSCDI&rft_id=info:doi/10.1016/j.tcs.2011.02.046&rft_dat=%3Cproquest_cross%3E907939076%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c402t-4bc663a30710175d6f4538eba97553690bf661646e710800ac27de32106761d63%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=907939076&rft_id=info:pmid/&rfr_iscdi=true |