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
Model abstraction for discrete-event systems using a SAT solver
School of Electro-Mechanical Engineering, Xidian University, Xi’an, China.
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.ORCID iD: 0000-0001-5703-5923
2023 (English)In: IEEE Access, E-ISSN 2169-3536, Vol. 11, p. 17334-17347Article in journal (Refereed) Published
Abstract [en]

Model abstraction for finite state automata is beneficial to reduce the complexity of discrete-event systems (DES), enhances the readability and facilitates the control synthesis and verification of DES. Supremal quasi-congruence computation is an effective way for reducing the state space of DES. Effective algorithms on the supremal quasi-congruence relation have been developed based on the graph theory. This paper proposes a new approach to translate the supremal quasi-congruence computation into a satisfiability (SAT) problem that determines whether there exists an assignment for Boolean variables in the state-to-coset allocation matrix. If the result is satisfied, then the supremal quasi-congruence relation exists and the minimum equivalence classes is obtained. Otherwise, it indicates that there is no such supremal quasi-congruence relation, and a new set of observable events needs to be modified or reselected for the original system model. The satisfiability problem on the computation of supremal quasi-congruence relation is solved by different methods, which are respectively implemented by mixed integer linear programming (MILP) in MATLAB, binary linear programming (BLP) in CPLEX, and a SAT-based solver (Z3Py). Compared with the MILP and BLP methods, the SAT method is more efficient and stable. The computation time of model abstraction for large-scale systems by Z3Py solver is significantly reduced.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE) , 2023. Vol. 11, p. 17334-17347
Keywords [en]
Discrete-event systems; Deterministic finite automata; Model abstraction; Satisfiability; Supremal Quasi-congruence relation
National Category
Computer Sciences Discrete Mathematics Computer Systems Control Engineering
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-324253DOI: 10.1109/access.2023.3246123ISI: 000939929400001Scopus ID: 2-s2.0-85149173421OAI: oai:DiVA.org:kth-324253DiVA, id: diva2:1739177
Funder
KTH Royal Institute of Technology, XPRES
Note

QC 20230228

Available from: 2023-02-24 Created: 2023-02-24 Last updated: 2023-03-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Feng, Lei

Search in DiVA

By author/editor
Feng, Lei
By organisation
Mechatronics
In the same journal
IEEE Access
Computer SciencesDiscrete MathematicsComputer SystemsControl Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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