Change search
ReferencesLink to record
Permanent link

Direct link
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 (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.
, 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
URN: urn:nbn:se:kth:diva-152708DOI: 10.1007/978-3-642-04761-9_6ISI: 000273514700005ScopusID: 2-s2.0-71549125591ISBN: 3642047602ISBN: 978-364204760-2OAI: diva2:752646
7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009; Macao; China; 14 October 2009 through 16 October 2009

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

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
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

Altmetric score

Total: 20 hits
ReferencesLink to record
Permanent link

Direct link