Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • 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 data symmetry reduction technique for temporal-epistemic logic
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.ORCID iD: 0000-0001-5432-6442
2009 (English)In: Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, Springer Berlin/Heidelberg, 2009, 69-83 p.Conference paper, Published paper (Refereed)
Abstract [en]

We present a data symmetry reduction approach for model checking temporal-epistemic logic. The technique abstracts the epistemic indistinguishably relation for the knowledge operators, and is shown to preserve temporal-epistemic formulae. We show a method for statically detecting data symmetry in an ISPL program, the input to the temporal-epistemic model checker MCMAS. The experiments we report show an exponential saving in verification time and space while verifying security properties of the NSPK protocol.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2009. 69-83 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5799
Keyword [en]
Epistemic logic, Model checker, NSPK protocol, Security properties, Symmetry reduction, Time and space, Network protocols, Network security, Temporal logic, Model checking
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-152708DOI: 10.1007/978-3-642-04761-9_6ISI: 000273514700005Scopus ID: 2-s2.0-71549125591ISBN: 3642047602 (print)ISBN: 978-364204760-2 OAI: oai:DiVA.org:kth-152708DiVA: diva2:752646
Conference
7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009; Macao; China; 14 October 2009 through 16 October 2009
Note

QC 20141006

Available from: 2014-10-06 Created: 2014-10-01 Last updated: 2014-10-06Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Dam, Mads

Search in DiVA

By author/editor
Dam, Mads
By organisation
Theoretical Computer Science, TCSACCESS Linnaeus Centre
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • 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