kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions
School of Computation, Information and Technology, Technical University of Munich, School of Computation, Information and Technology, Technical University of Munich; School of Computer Science and Engineering, Constructor University, School of Computer Science and Engineering, Constructor University.
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). (Digital Futures)ORCID iD: 0000-0001-6653-5508
School of Computer Science and Engineering, Constructor University, School of Computer Science and Engineering, Constructor University.
KTH, School of Electrical Engineering and Computer Science (EECS), Intelligent systems, Decision and Control Systems (Automatic Control). (Digital Futures)ORCID iD: 0000-0001-9940-5929
2023 (English)In: 2023 62nd IEEE Conference on Decision and Control, CDC 2023, Institute of Electrical and Electronics Engineers (IEEE) , 2023, p. 60-66Conference paper, Published paper (Refereed)
Abstract [en]

A logical zonotope, which is a new set representation for binary vectors, is introduced in this paper. A logical zonotope is constructed by XORing a binary vector with a combination of other binary vectors called generators. Such a zonotope can represent up to 2γ binary vectors using only γ generators. It is shown that logical operations over sets of binary vectors can be performed on the zonotopes' generators and, thus, significantly reduce the computational complexity of various logical operations (e.g., XOR, NAND, AND, OR, and semi-tensor products). Similar to traditional zonotopes' role in the formal verification of dynamical systems over real vector spaces, logical zonotopes can efficiently analyze discrete dynamical systems defined over binary vector spaces. We illustrate the approach and its ability to reduce the computational complexity in two use cases: (1) encryption key discovery of a linear feedback shift register and (2) safety verification of a road traffic intersection protocol.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2023. p. 60-66
Series
Proceedings of the IEEE Conference on Decision and Control, ISSN 0743-1546
National Category
Discrete Mathematics
Identifiers
URN: urn:nbn:se:kth:diva-343723DOI: 10.1109/CDC49753.2023.10384037ISI: 001166433800009Scopus ID: 2-s2.0-85184806966OAI: oai:DiVA.org:kth-343723DiVA, id: diva2:1839918
Conference
62nd IEEE Conference on Decision and Control, CDC 2023, Singapore, Singapore, Dec 13 2023 - Dec 15 2023
Note

QC 20240226

Part of ISBN 9798350301243

Available from: 2024-02-22 Created: 2024-02-22 Last updated: 2024-03-26Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Jiang, FrankJohansson, Karl H.

Search in DiVA

By author/editor
Jiang, FrankJohansson, Karl H.
By organisation
Decision and Control Systems (Automatic Control)
Discrete Mathematics

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • 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