Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
A data symmetry reduction technique for temporal-epistemic logic
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.ORCID-id: 0000-0001-5432-6442
2009 (engelsk)Inngår i: Automated Technology for Verification and Analysis: 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, Springer Berlin/Heidelberg, 2009, 69-83 s.Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Springer Berlin/Heidelberg, 2009. 69-83 s.
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5799
Emneord [en]
Epistemic logic, Model checker, NSPK protocol, Security properties, Symmetry reduction, Time and space, Network protocols, Network security, Temporal logic, Model checking
HSV kategori
Identifikatorer
URN: urn:nbn:se:kth:diva-152708DOI: 10.1007/978-3-642-04761-9_6ISI: 000273514700005Scopus ID: 2-s2.0-71549125591ISBN: 3642047602 (tryckt)ISBN: 978-364204760-2 OAI: oai:DiVA.org:kth-152708DiVA: diva2:752646
Konferanse
7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009; Macao; China; 14 October 2009 through 16 October 2009
Merknad

QC 20141006

Tilgjengelig fra: 2014-10-06 Laget: 2014-10-01 Sist oppdatert: 2018-01-11bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler

Andre lenker

Forlagets fulltekstScopus

Personposter BETA

Dam, Mads

Søk i DiVA

Av forfatter/redaktør
Dam, Mads
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 29 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf