Computer-Aided Verification of Coordinating Processes : : The Automata-Theoretic Approach / / Robert P. Kurshan.
Formal verification increasingly has become recognized as an answer to the problem of how to create ever more complex control systems, which nonetheless are required to behave reliably. To be acceptable in an industrial setting, formal verification must be highly algorithmic; to cope with design com...
Saved in:
Superior document: | Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package 1980-1999 |
---|---|
VerfasserIn: | |
Place / Publishing House: | Princeton, NJ : : Princeton University Press, , [2014] ©1995 |
Year of Publication: | 2014 |
Edition: | Course Book |
Language: | English |
Series: | Princeton Readings in Religions ;
302 |
Online Access: | |
Physical Description: | 1 online resource (284 p.) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
9781400864041 |
---|---|
ctrlnum |
(DE-B1597)447425 (OCoLC)979578773 |
collection |
bib_alma |
record_format |
marc |
spelling |
Kurshan, Robert P., author. aut http://id.loc.gov/vocabulary/relators/aut Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / Robert P. Kurshan. Course Book Princeton, NJ : Princeton University Press, [2014] ©1995 1 online resource (284 p.) text txt rdacontent computer c rdamedia online resource cr rdacarrier text file PDF rda Princeton Readings in Religions ; 302 Frontmatter -- Contents -- Preface -- Chapter 1. Introduction -- Chapter 2. Boolean Algebra -- Chapter 3. L-matrix -- Chapter 4. L-language -- Chapter 5. String Acceptors -- Chapter 6. ω-theory: L-automaton/L-process -- Chapter 7. The Selection/Resolution Model of Coordinating Processes -- Chapter 8. Reduction of Verification -- Chapter 9. Structural Induction -- Chapter 10. Binary Decision Diagrams -- Appendices -- Bibliography -- Glossary -- Index -- Backmatter restricted access http://purl.org/coar/access_right/c_16ec online access with authorization star Formal verification increasingly has become recognized as an answer to the problem of how to create ever more complex control systems, which nonetheless are required to behave reliably. To be acceptable in an industrial setting, formal verification must be highly algorithmic; to cope with design complexity, it must support a top-down design methodology that leads from an abstract design to its detailed implementation. That combination of requirements points directly to the widely recognized solution of automata-theoretic verification, on account of its expressiveness, computational complexity, and perhaps general utility as well.This book develops the theory of automata-theoretic verification from its foundations, with a focus on algorithms and heuristics to reduce the computational complexity of analysis. It is suitable as a text for a one-or two-semester graduate course, and is recommended reading for anyone planning to use a verification tool, such as COSPAN or SMV. An extensive bibliography that points to the most recent sources, and extensive discussions of methodology and comparisons with other techniques, make this a useful resource for research or verification tool development, as well.Originally published in 1995.The Princeton Legacy Library uses the latest print-on-demand technology to again make available previously out-of-print books from the distinguished backlist of Princeton University Press. These editions preserve the original texts of these important books while presenting them in durable paperback and hardcover editions. The goal of the Princeton Legacy Library is to vastly increase access to the rich scholarly heritage found in the thousands of books published by Princeton University Press since its founding in 1905. Issued also in print. Mode of access: Internet via World Wide Web. In English. Description based on online resource; title from PDF title page (publisher's Web site, viewed 30. Aug 2021) MATHEMATICS / Complex Analysis. bisacsh Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package 1980-1999 9783110413441 Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package Science 9783110413595 Title is part of eBook package: De Gruyter Princeton University Press eBook-Package Archive 1927-1999 9783110442496 print 9780691606057 https://doi.org/10.1515/9781400864041 https://www.degruyter.com/isbn/9781400864041 Cover https://www.degruyter.com/cover/covers/9781400864041.jpg |
language |
English |
format |
eBook |
author |
Kurshan, Robert P., Kurshan, Robert P., |
spellingShingle |
Kurshan, Robert P., Kurshan, Robert P., Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / Princeton Readings in Religions ; Frontmatter -- Contents -- Preface -- Chapter 1. Introduction -- Chapter 2. Boolean Algebra -- Chapter 3. L-matrix -- Chapter 4. L-language -- Chapter 5. String Acceptors -- Chapter 6. ω-theory: L-automaton/L-process -- Chapter 7. The Selection/Resolution Model of Coordinating Processes -- Chapter 8. Reduction of Verification -- Chapter 9. Structural Induction -- Chapter 10. Binary Decision Diagrams -- Appendices -- Bibliography -- Glossary -- Index -- Backmatter |
author_facet |
Kurshan, Robert P., Kurshan, Robert P., |
author_variant |
r p k rp rpk r p k rp rpk |
author_role |
VerfasserIn VerfasserIn |
author_sort |
Kurshan, Robert P., |
title |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / |
title_sub |
The Automata-Theoretic Approach / |
title_full |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / Robert P. Kurshan. |
title_fullStr |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / Robert P. Kurshan. |
title_full_unstemmed |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / Robert P. Kurshan. |
title_auth |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / |
title_alt |
Frontmatter -- Contents -- Preface -- Chapter 1. Introduction -- Chapter 2. Boolean Algebra -- Chapter 3. L-matrix -- Chapter 4. L-language -- Chapter 5. String Acceptors -- Chapter 6. ω-theory: L-automaton/L-process -- Chapter 7. The Selection/Resolution Model of Coordinating Processes -- Chapter 8. Reduction of Verification -- Chapter 9. Structural Induction -- Chapter 10. Binary Decision Diagrams -- Appendices -- Bibliography -- Glossary -- Index -- Backmatter |
title_new |
Computer-Aided Verification of Coordinating Processes : |
title_sort |
computer-aided verification of coordinating processes : the automata-theoretic approach / |
series |
Princeton Readings in Religions ; |
series2 |
Princeton Readings in Religions ; |
publisher |
Princeton University Press, |
publishDate |
2014 |
physical |
1 online resource (284 p.) Issued also in print. |
edition |
Course Book |
contents |
Frontmatter -- Contents -- Preface -- Chapter 1. Introduction -- Chapter 2. Boolean Algebra -- Chapter 3. L-matrix -- Chapter 4. L-language -- Chapter 5. String Acceptors -- Chapter 6. ω-theory: L-automaton/L-process -- Chapter 7. The Selection/Resolution Model of Coordinating Processes -- Chapter 8. Reduction of Verification -- Chapter 9. Structural Induction -- Chapter 10. Binary Decision Diagrams -- Appendices -- Bibliography -- Glossary -- Index -- Backmatter |
isbn |
9781400864041 9783110413441 9783110413595 9783110442496 9780691606057 |
url |
https://doi.org/10.1515/9781400864041 https://www.degruyter.com/isbn/9781400864041 https://www.degruyter.com/cover/covers/9781400864041.jpg |
illustrated |
Not Illustrated |
doi_str_mv |
10.1515/9781400864041 |
oclc_num |
979578773 |
work_keys_str_mv |
AT kurshanrobertp computeraidedverificationofcoordinatingprocessestheautomatatheoreticapproach |
status_str |
n |
ids_txt_mv |
(DE-B1597)447425 (OCoLC)979578773 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package 1980-1999 Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package Science Title is part of eBook package: De Gruyter Princeton University Press eBook-Package Archive 1927-1999 |
is_hierarchy_title |
Computer-Aided Verification of Coordinating Processes : The Automata-Theoretic Approach / |
container_title |
Title is part of eBook package: De Gruyter Princeton Legacy Lib. eBook Package 1980-1999 |
_version_ |
1770176714073178112 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>05115nam a22007215i 4500</leader><controlfield tag="001">9781400864041</controlfield><controlfield tag="003">DE-B1597</controlfield><controlfield tag="005">20210830012106.0</controlfield><controlfield tag="006">m|||||o||d||||||||</controlfield><controlfield tag="007">cr || ||||||||</controlfield><controlfield tag="008">210830t20141995nju fo d z eng d</controlfield><datafield tag="019" ind1=" " ind2=" "><subfield code="a">(OCoLC)984653373</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9781400864041</subfield></datafield><datafield tag="024" ind1="7" ind2=" "><subfield code="a">10.1515/9781400864041</subfield><subfield code="2">doi</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(DE-B1597)447425</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)979578773</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">DE-B1597</subfield><subfield code="b">eng</subfield><subfield code="c">DE-B1597</subfield><subfield code="e">rda</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="044" ind1=" " ind2=" "><subfield code="a">nju</subfield><subfield code="c">US-NJ</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">MAT040000</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Kurshan, Robert P., </subfield><subfield code="e">author.</subfield><subfield code="4">aut</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/aut</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Computer-Aided Verification of Coordinating Processes :</subfield><subfield code="b">The Automata-Theoretic Approach /</subfield><subfield code="c">Robert P. Kurshan.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">Course Book</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Princeton, NJ : </subfield><subfield code="b">Princeton University Press, </subfield><subfield code="c">[2014]</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©1995</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (284 p.)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="347" ind1=" " ind2=" "><subfield code="a">text file</subfield><subfield code="b">PDF</subfield><subfield code="2">rda</subfield></datafield><datafield tag="490" ind1="0" ind2=" "><subfield code="a">Princeton Readings in Religions ;</subfield><subfield code="v">302</subfield></datafield><datafield tag="505" ind1="0" ind2="0"><subfield code="t">Frontmatter -- </subfield><subfield code="t">Contents -- </subfield><subfield code="t">Preface -- </subfield><subfield code="t">Chapter 1. Introduction -- </subfield><subfield code="t">Chapter 2. Boolean Algebra -- </subfield><subfield code="t">Chapter 3. L-matrix -- </subfield><subfield code="t">Chapter 4. L-language -- </subfield><subfield code="t">Chapter 5. String Acceptors -- </subfield><subfield code="t">Chapter 6. ω-theory: L-automaton/L-process -- </subfield><subfield code="t">Chapter 7. The Selection/Resolution Model of Coordinating Processes -- </subfield><subfield code="t">Chapter 8. Reduction of Verification -- </subfield><subfield code="t">Chapter 9. Structural Induction -- </subfield><subfield code="t">Chapter 10. Binary Decision Diagrams -- </subfield><subfield code="t">Appendices -- </subfield><subfield code="t">Bibliography -- </subfield><subfield code="t">Glossary -- </subfield><subfield code="t">Index -- </subfield><subfield code="t">Backmatter</subfield></datafield><datafield tag="506" ind1="0" ind2=" "><subfield code="a">restricted access</subfield><subfield code="u">http://purl.org/coar/access_right/c_16ec</subfield><subfield code="f">online access with authorization</subfield><subfield code="2">star</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">Formal verification increasingly has become recognized as an answer to the problem of how to create ever more complex control systems, which nonetheless are required to behave reliably. To be acceptable in an industrial setting, formal verification must be highly algorithmic; to cope with design complexity, it must support a top-down design methodology that leads from an abstract design to its detailed implementation. That combination of requirements points directly to the widely recognized solution of automata-theoretic verification, on account of its expressiveness, computational complexity, and perhaps general utility as well.This book develops the theory of automata-theoretic verification from its foundations, with a focus on algorithms and heuristics to reduce the computational complexity of analysis. It is suitable as a text for a one-or two-semester graduate course, and is recommended reading for anyone planning to use a verification tool, such as COSPAN or SMV. An extensive bibliography that points to the most recent sources, and extensive discussions of methodology and comparisons with other techniques, make this a useful resource for research or verification tool development, as well.Originally published in 1995.The Princeton Legacy Library uses the latest print-on-demand technology to again make available previously out-of-print books from the distinguished backlist of Princeton University Press. These editions preserve the original texts of these important books while presenting them in durable paperback and hardcover editions. The goal of the Princeton Legacy Library is to vastly increase access to the rich scholarly heritage found in the thousands of books published by Princeton University Press since its founding in 1905.</subfield></datafield><datafield tag="530" ind1=" " ind2=" "><subfield code="a">Issued also in print.</subfield></datafield><datafield tag="538" ind1=" " ind2=" "><subfield code="a">Mode of access: Internet via World Wide Web.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">In English.</subfield></datafield><datafield tag="588" ind1="0" ind2=" "><subfield code="a">Description based on online resource; title from PDF title page (publisher's Web site, viewed 30. Aug 2021)</subfield></datafield><datafield tag="650" ind1=" " ind2="7"><subfield code="a">MATHEMATICS / Complex Analysis.</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">Princeton Legacy Lib. eBook Package 1980-1999</subfield><subfield code="z">9783110413441</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">Princeton Legacy Lib. eBook Package Science</subfield><subfield code="z">9783110413595</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">Princeton University Press eBook-Package Archive 1927-1999</subfield><subfield code="z">9783110442496</subfield></datafield><datafield tag="776" ind1="0" ind2=" "><subfield code="c">print</subfield><subfield code="z">9780691606057</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://doi.org/10.1515/9781400864041</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://www.degruyter.com/isbn/9781400864041</subfield></datafield><datafield tag="856" ind1="4" ind2="2"><subfield code="3">Cover</subfield><subfield code="u">https://www.degruyter.com/cover/covers/9781400864041.jpg</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-041344-1 Princeton Legacy Lib. eBook Package 1980-1999</subfield><subfield code="c">1980</subfield><subfield code="d">1999</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-041359-5 Princeton Legacy Lib. eBook Package Science</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-044249-6 Princeton University Press eBook-Package Archive 1927-1999</subfield><subfield code="c">1927</subfield><subfield code="d">1999</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_BACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_CL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ECL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EEBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ESTMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_PPALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_STMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">GBV-deGruyter-alles</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA12STME</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA13ENGE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA18STMEE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA5EBK</subfield></datafield></record></collection> |