RCTL: New Temporal Logic for Improved Formal Verification of Reconfigurable Discrete-Event Systems

Mohamed Ramdani, Laid Kahloul, Mohamed Khalgui, Zhiwu Li, Meng Chu Zhou

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

Abstract

This article deals with improved formal verification of reconfigurable discrete-event systems (DESs) modeled by reconfigurable timed net condition event systems (R-TNCESs). An R-TNCES consists of a set of timed net condition event systems, each of which represents a particular behavior of a DES, and a reconfiguration scenario is a switching mode from a timed net condition event system to another. However, the verification with the classical computation tree logic (CTL) as well as the related extensions increases the number of properties for complete verification of a complex R-TNCES. We propose reconfigurable CTL as a new extension of CTL to reduce such a number. New connectors of reconfigurable CTL are proposed, with their formal syntax and semantics, and a set of new algorithms is proposed to control the complexity of model checking. We use a benchmark production system for the performance evaluation of the proposed approach. Reduction in the number of properties to be checked is shown, and consequently, the related validation time is reduced. Note to Practitioners - This research represents a new orientation for guiding efficiently the model checking of reconfigurable discrete-event systems. A classification of properties described in computation tree logic (CTL), according to their dominance and equivalence relations, allows one to conduct an efficient verification by avoiding inefficient calculation due to redundant properties. In this case, giving a verification order for these properties allows one to shorten their verification time. An extension named reconfigurable CTL describes the new syntax of the proposed classification. This approach can be applied in modeling and verification of advanced reconfigurable systems arising from smart grids, adaptive sensor networks, intelligent transportation, reconfigurable manufacturing, and embedded systems.

Original languageEnglish (US)
Article number9149784
Pages (from-to)1392-1405
Number of pages14
JournalIEEE Transactions on Automation Science and Engineering
Volume18
Issue number3
DOIs
StatePublished - Jul 2021
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Keywords

  • Computation tree logic (CTL)
  • discrete-event system (DES)
  • model checking
  • Petri net
  • reconfigurable CTL (RCTL)
  • reconfigurable timed net condition event system (R-TNCES)
  • reconfiguration

Fingerprint

Dive into the research topics of 'RCTL: New Temporal Logic for Improved Formal Verification of Reconfigurable Discrete-Event Systems'. Together they form a unique fingerprint.

Cite this