## Partial Order Methods in Verification: DIMACS Workshop, July 24-26, 1996Doron Peled, Vaughan R. Pratt, Gerard J. Holzmann This book presents surveys on the theory and practice of modeling, specifying, and validating concurrent systems. It contains surveys of techniques used in tools developed for automatic validation of systems. Other papers present recent developments in concurrency theory, logics of programs, model-checking, automata, and formal languages theory. The volume contains the proceedings from the workshop, Partial Order Methods in Verification, which was held in Princeton, NJ, in July 1996. The workshop focused on both the practical and the theoretical aspects of using partial order models, including automata and formal languages, category theory, concurrency theory, logic, process algebra, program semantics, specification and verification, topology, and trace theory. The book also includes a lively e-mail debate that took place about the importance of the partial order dichotomy in modeling concurrency. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Elements of an automata theory over partial orders | 25 |

Algebraic manipulations and vector languages | 41 |

Refinement with global equivalence proofs in temporal logic | 59 |

A complete axiomatization of a firstorder temporal logic over trace systems | 79 |

Interleaved progress concurrent progress and local progress | 99 |

Teams can see pomsets | 117 |

On topological hierarchies of temporal properties | 141 |

Linear time temporal logics over Mazurkiewicz traces | 171 |

Linear and branching temporal logics and process | 233 |

History dependent verification for partial order systems | 259 |

Transition systems with independence and multiarcs | 273 |

On the costs and benefits of using partialorder methods for the verification | 289 |

Partial order verification with | 305 |

A language and toolset for simulation of distributed systems | 329 |

An electronic discussion on true concurrency | 359 |

A solution of an interleaving decision problem by a partial order technique | 203 |

### Other editions - View all

### Common terms and phrases

abstract actions algorithms alphabet architecture atomic automaton behavior bisimilar bisimulation causal automata checking compact elements component concurrent programs concurrent run concurrent systems condition consider constraints construction corresponding defined Definition denote dependency distributed domain elements equivalence relation es-net event structures example execution sequences exists expressive formal formula global graph acceptor Hence implementation independence relation initial interface interleaving isomorphism labelled lats Lecture Notes Lemma linear time model LNCS loc(a Mathematics model-checking modules monoid morphisms multiset Notes in Computer notion observation occurrence operations partial computations partial order partial order reduction partial-order methods path Peled Petri nets pomset language pomsets prefix functions presheaves problem Proc proof properties Proposition queue reachable reduced LTS result satisfies second-order logic sequentially consistent Springer-Verlag state-space string stubborn set subset systems with independence temporal logic Theorem Theoretical Computer Science theory transition relation TrPTL TSIm variables Vaughan Pratt verification x-path