Automatic synthesis for the reachability of process systems with a model checking algorithm

Jinkyung Kim, Jaedeuk Park, Il Moon

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


This study focuses on the applications of model checking techniques in automatic synthesis for the reachability of process systems. Model checking is an automatic method used to verify if a circuit or a condition, expressed as a concurrent transition system, satisfies a set of properties. The strength of this method lies in its ability to synthesize a feasible sequence with a counterexample and to verify its correctness using temporal logics such as computation tree logic (CTL) simultaneously. These challengeable approaches are implemented in a commercial software package (UPPAAL) using graphical discrete modeling, automata theory, and CTL to automate the synthesis for the reachability of process systems. Three use cases of interest in computer-aided engineering due to the difficulty involved in synthesizing them manually are explored. In the first use case, the optimal operating procedure according to the objective function of a paper mill process is synthesized. In the second use case, a challengeable attempt to optimize supply chain networks is tested. In the third use case, alternative pathways with the desired constraints are found in biochemical networks. The paper also explains how the proposed model checking method can be used efficiently in graphical modeling with automata theory to automatically synthesize process systems counterexamples using CTL by means of the case studies.

Original languageEnglish
Pages (from-to)2613-2624
Number of pages12
JournalIndustrial and Engineering Chemistry Research
Issue number7
Publication statusPublished - 2013 Feb 20

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Automatic synthesis for the reachability of process systems with a model checking algorithm'. Together they form a unique fingerprint.

Cite this