uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A general approach to partial order reductions in symbolic verification
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
1998 (English)In: Computer Aided Verification: Proceedings of CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, 379-390 p.Conference paper, Published paper (Refereed)
Abstract [en]

The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.

We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.

Place, publisher, year, edition, pages
1998. Vol. 1427, 379-390 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 1427
Keyword [en]
model-checking, algorithms, atomicity
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-27322DOI: 10.1007/BFb0028760ISBN: 978-3-540-64608-2 (print)ISBN: 978-3-540-69339-0 (print)OAI: oai:DiVA.org:uu-27322DiVA: diva2:55217
Conference
10th International Conference, CAV'98 Vancouver, BC, Canada, June 28 – July 2, 1998
Available from: 2008-10-17 Created: 2008-10-17 Last updated: 2013-10-03Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Abdulla, Parosh AzizJonsson, Bengt

Search in DiVA

By author/editor
Abdulla, Parosh AzizJonsson, Bengt
By organisation
Department of Computer Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 465 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf