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
Regular Symmetry Patterns
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)ORCID iD: 0000-0002-2733-7098
2016 (English)In: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2016, 455-475 p.Conference paper, Published paper (Refereed)
Abstract [en]

Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We propose a symbolic framework for capturing symmetry patterns in parameterised systems (i.e. an infinite family of finite-state systems): two regular word transducers to represent, respectively, parameterised systems and symmetry patterns. The framework subsumes various types of "symmetry relations" ranging from weaker notions (e.g. simulation preorders) to the strongest notion (i.e. isomorphisms). Our framework enjoys two algorithmic properties: (1) symmetry verification: given a transducer, we can automatically check whether it is a symmetry pattern of a given system, and (2) symmetry synthesis: we can automatically generate a symmetry pattern for a given system in the form of a transducer. Furthermore, our symbolic language allows additional constraints that the symmetry patterns need to satisfy to be easily incorporated in the verification/synthesis. We show how these properties can help identify symmetry patterns in examples like dining philosopher protocols, self-stabilising protocols, and prioritised resource-allocator protocol. In some cases (e.g. Gries's coffee can problem), our technique automatically synthesises a safety-preserving finite approximant, which can then be verified for safety solely using a finite-state model checker.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016. 455-475 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9583
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-287501DOI: 10.1007/978-3-662-49122-5_22ISI: 000375148800022ISBN: 9783662491218 (print)OAI: oai:DiVA.org:uu-287501DiVA: diva2:922858
Conference
VMCAI 2016, January 17–19, Saint Petersburg, FL
Projects
UPMARC
Funder
Swedish Research Council, 2014-5484
Available from: 2015-12-25 Created: 2016-04-25 Last updated: 2016-07-26Bibliographically approved

Open Access in DiVA

fulltext(377 kB)48 downloads
File information
File name FULLTEXT01.pdfFile size 377 kBChecksum SHA-512
9e2df616c5f867b07b752bc30d17f114f9ea6ed9708d37dacd0d5a07ce5142d63b9b4f2134486c7b8ec219b6a90f6bb68f1f3be8eeed943d2bf389a44695dff1
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Rümmer, Philipp

Search in DiVA

By author/editor
Rümmer, Philipp
By organisation
Computer Systems
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 48 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 195 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