Model checking of real-time properties of resource-bound process algebra

Junkil Park, Jungjae Lee, Jin Young Choi, Insup Lee

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


The algebra of communicating shared resources (ACSR) is a timed process algebra which extends classical process algebras with the notion of a resource. In analyzing ACSR models, the existing techniques such as bisimulation checking and Hennessy-Milner Logic (HML) model checking are very important in theory of ACSR, but they are di fficult to use for large complex system models in practice. In this paper, we suggest a framework to verify ACSR models against their requirements described in an expressive timed temporal logic. We demonstrate the usefulness of our approach with a real world case study.

Original languageEnglish
Pages (from-to)2781-2789
Number of pages9
JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
Issue number11
Publication statusPublished - 2009 Nov


  • ACSR
  • Action-based modeling
  • Model checking
  • Real-time temporal logic
  • Resource-bound process algebra

ASJC Scopus subject areas

  • Signal Processing
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering
  • Applied Mathematics


Dive into the research topics of 'Model checking of real-time properties of resource-bound process algebra'. Together they form a unique fingerprint.

Cite this