Computational effort of BDD-based supervisor synthesis of extended finite automata

Sander Thuijsman, D. Hendriks, R.J.M. Theunissen, Michel Reniers, Ramon Schiffelers

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

We consider supervisor synthesis of Extended Finite Automata that are represented using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as platform independent and deterministic metrics that quantitatively indicate the computational effort needed to synthesize a supervisor. The use of BDD operation count is novel with respect to expressing supervisor synthesis effort. The (dis-)advantages of using these metrics to state of practice metrics such as wall clock time and worst case state space size are analyzed. The supervisor synthesis algorithm is initiated with a certain event- and variable order. It is already known from literature that variable order influences synthesis performance. We show that the event order is also relevant to consider. We discuss how these orders influence the synthesis effort and, by performing an experiment on a set of models, we show the extent of this influence.
LanguageEnglish
Title of host publication2019 IEEE 15th International Conference on Automation Science and Engineering
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Pages486-493
Number of pages8
ISBN (Electronic)978-1-7281-0356-3
DOIs
StatePublished - 2019
Event15th IEEE International Conference on Automation Science and Engineering, (CASE 2019) - University of British Columbia, Vancouver, Canada
Duration: 22 Aug 201926 Aug 2019
Conference number: 15
http://case2019.hust.edu.cn/

Conference

Conference15th IEEE International Conference on Automation Science and Engineering, (CASE 2019)
Abbreviated titleCASE2019
CountryCanada
CityVancouver
Period22/08/1926/08/19
Internet address

Fingerprint

Binary decision diagrams
Supervisory personnel
Finite automata
Clocks
Experiments

Cite this

Thuijsman, S., Hendriks, D., Theunissen, R. J. M., Reniers, M., & Schiffelers, R. (2019). Computational effort of BDD-based supervisor synthesis of extended finite automata. In 2019 IEEE 15th International Conference on Automation Science and Engineering (pp. 486-493). Piscataway: Institute of Electrical and Electronics Engineers. DOI: 10.1109/COASE.2019.8843327
Thuijsman, Sander ; Hendriks, D. ; Theunissen, R.J.M. ; Reniers, Michel ; Schiffelers, Ramon. / Computational effort of BDD-based supervisor synthesis of extended finite automata. 2019 IEEE 15th International Conference on Automation Science and Engineering. Piscataway : Institute of Electrical and Electronics Engineers, 2019. pp. 486-493
@inproceedings{dbae3ec2d78647a28588c30a483a4365,
title = "Computational effort of BDD-based supervisor synthesis of extended finite automata",
abstract = "We consider supervisor synthesis of Extended Finite Automata that are represented using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as platform independent and deterministic metrics that quantitatively indicate the computational effort needed to synthesize a supervisor. The use of BDD operation count is novel with respect to expressing supervisor synthesis effort. The (dis-)advantages of using these metrics to state of practice metrics such as wall clock time and worst case state space size are analyzed. The supervisor synthesis algorithm is initiated with a certain event- and variable order. It is already known from literature that variable order influences synthesis performance. We show that the event order is also relevant to consider. We discuss how these orders influence the synthesis effort and, by performing an experiment on a set of models, we show the extent of this influence.",
author = "Sander Thuijsman and D. Hendriks and R.J.M. Theunissen and Michel Reniers and Ramon Schiffelers",
year = "2019",
doi = "10.1109/COASE.2019.8843327",
language = "English",
pages = "486--493",
booktitle = "2019 IEEE 15th International Conference on Automation Science and Engineering",
publisher = "Institute of Electrical and Electronics Engineers",
address = "United States",

}

Thuijsman, S, Hendriks, D, Theunissen, RJM, Reniers, M & Schiffelers, R 2019, Computational effort of BDD-based supervisor synthesis of extended finite automata. in 2019 IEEE 15th International Conference on Automation Science and Engineering. Institute of Electrical and Electronics Engineers, Piscataway, pp. 486-493, 15th IEEE International Conference on Automation Science and Engineering, (CASE 2019), Vancouver, Canada, 22/08/19. DOI: 10.1109/COASE.2019.8843327

Computational effort of BDD-based supervisor synthesis of extended finite automata. / Thuijsman, Sander; Hendriks, D.; Theunissen, R.J.M.; Reniers, Michel; Schiffelers, Ramon.

2019 IEEE 15th International Conference on Automation Science and Engineering. Piscataway : Institute of Electrical and Electronics Engineers, 2019. p. 486-493.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Computational effort of BDD-based supervisor synthesis of extended finite automata

AU - Thuijsman,Sander

AU - Hendriks,D.

AU - Theunissen,R.J.M.

AU - Reniers,Michel

AU - Schiffelers,Ramon

PY - 2019

Y1 - 2019

N2 - We consider supervisor synthesis of Extended Finite Automata that are represented using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as platform independent and deterministic metrics that quantitatively indicate the computational effort needed to synthesize a supervisor. The use of BDD operation count is novel with respect to expressing supervisor synthesis effort. The (dis-)advantages of using these metrics to state of practice metrics such as wall clock time and worst case state space size are analyzed. The supervisor synthesis algorithm is initiated with a certain event- and variable order. It is already known from literature that variable order influences synthesis performance. We show that the event order is also relevant to consider. We discuss how these orders influence the synthesis effort and, by performing an experiment on a set of models, we show the extent of this influence.

AB - We consider supervisor synthesis of Extended Finite Automata that are represented using Binary Decision Diagrams (BDDs). Peak used BDD nodes and BDD operation count are introduced as platform independent and deterministic metrics that quantitatively indicate the computational effort needed to synthesize a supervisor. The use of BDD operation count is novel with respect to expressing supervisor synthesis effort. The (dis-)advantages of using these metrics to state of practice metrics such as wall clock time and worst case state space size are analyzed. The supervisor synthesis algorithm is initiated with a certain event- and variable order. It is already known from literature that variable order influences synthesis performance. We show that the event order is also relevant to consider. We discuss how these orders influence the synthesis effort and, by performing an experiment on a set of models, we show the extent of this influence.

U2 - 10.1109/COASE.2019.8843327

DO - 10.1109/COASE.2019.8843327

M3 - Conference contribution

SP - 486

EP - 493

BT - 2019 IEEE 15th International Conference on Automation Science and Engineering

PB - Institute of Electrical and Electronics Engineers

CY - Piscataway

ER -

Thuijsman S, Hendriks D, Theunissen RJM, Reniers M, Schiffelers R. Computational effort of BDD-based supervisor synthesis of extended finite automata. In 2019 IEEE 15th International Conference on Automation Science and Engineering. Piscataway: Institute of Electrical and Electronics Engineers. 2019. p. 486-493. Available from, DOI: 10.1109/COASE.2019.8843327