More stubborn set methods for process algebras
Research output: Chapter in Book/Report/Conference proceeding › Chapter › Scientific
Details
| Original language | English |
|---|---|
| Title of host publication | Concurrency, Security, and Puzzles |
| Subtitle of host publication | Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday |
| Editors | Thomas Gibson-Robinson, Philippa Hopcroft, Ranko Lazić |
| Publisher | Springer International Publishing |
| Pages | 246-271 |
| Number of pages | 26 |
| ISBN (Electronic) | 978-3-319-51046-0 |
| ISBN (Print) | 978-3-319-51045-3 |
| DOIs | |
| Publication status | Published - 1 Jan 2017 |
| Publication type | B2 Part of a book or another research book |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 10160 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Abstract
Six stubborn set methods for computing reduced labelled transition systems are presented. Two of them preserve the traces, and one is tailored for on-the-fly verification of safety properties. The rest preserve the tree failures, fair testing equivalence, or the divergence traces. Two methods are entirely new, the ideas of three are recent and the adaptation to the process-algebraic setting with non-deterministic actions is new, and one is recent but slightly generalized. Most of the methods address problems in earlier solutions to the so-called ignoring problem. The correctness of each method is proven, and efficient implementation is discussed.