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

Jinkyung Kim, Jaedeuk Park, Il Moon

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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
Volume52
Issue number7
DOIs
Publication statusPublished - 2013 Feb 20

Fingerprint

Model checking
Automata theory
Temporal logic
Computer aided engineering
Software packages
Supply chains
Networks (circuits)

All Science Journal Classification (ASJC) codes

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

Cite this

@article{4c4565705dd84b3c8b6aca38083da2b4,
title = "Automatic synthesis for the reachability of process systems with a model checking algorithm",
abstract = "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.",
author = "Jinkyung Kim and Jaedeuk Park and Il Moon",
year = "2013",
month = "2",
day = "20",
doi = "10.1021/ie301758r",
language = "English",
volume = "52",
pages = "2613--2624",
journal = "Industrial & Engineering Chemistry Product Research and Development",
issn = "0888-5885",
publisher = "American Chemical Society",
number = "7",

}

Automatic synthesis for the reachability of process systems with a model checking algorithm. / Kim, Jinkyung; Park, Jaedeuk; Moon, Il.

In: Industrial and Engineering Chemistry Research, Vol. 52, No. 7, 20.02.2013, p. 2613-2624.

Research output: Contribution to journalArticle

TY - JOUR

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

AU - Kim, Jinkyung

AU - Park, Jaedeuk

AU - Moon, Il

PY - 2013/2/20

Y1 - 2013/2/20

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84874080989&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84874080989&partnerID=8YFLogxK

U2 - 10.1021/ie301758r

DO - 10.1021/ie301758r

M3 - Article

VL - 52

SP - 2613

EP - 2624

JO - Industrial & Engineering Chemistry Product Research and Development

JF - Industrial & Engineering Chemistry Product Research and Development

SN - 0888-5885

IS - 7

ER -