Using Maximality-Based Labeled Transition System Model for Concurrency Logic Verification

N. A.

doi:10.34028/iajit

Article Details

Using Maximality-Based Labeled Transition System Model for Concurrency Logic Verification

Authors:

N. A.

Publisher:

Zarqa University, Jordan

Journal:

The International Arab Journal of Information Technology (IAJIT) Vol.2 Issue 3, pp.23-29

Document Type:

Article

Publication Date:

1/2005

Document Language:

English

Document ID (Org No.):

2001388717

pISSN:

2309-4524

DOI:

10.34028/iajit

Keywords:

Abstract:

 In this paper, we show the interest of the maximality-based semantics for the check of concurrent system properties. For this purpose, we use the Maximality-based Labeled Transition System (MLTS) as a behavior model. From this point of view, we can omit action temporal and structural atomicity hypotheses; consequently, we can inherit result of combinatorial state space explosion problem solution based on the use of true concurrency semantics. Properties to be verified are expressed using the Computation Tree Logic (CTL). The main contribution of the paper is to show that model checking algorithms proposed in the literature, which are based on interleaving semantics, may be adapted easily to true concurrency semantics for the verification of new properties classes related to simultaneous progress of actions at different states.

Article Details

Using Maximality-Based Labeled Transition System Model for Concurrency Logic Verification

Authors:

N. A.

Publisher:

Zarqa University, Jordan

Journal:

The International Arab Journal of Information Technology (IAJIT) Vol.2 Issue 3, pp.23-29

Document Type:

Article

Publication Date:

1/2005

Document Language:

English

Document ID (Org No.):

2001388717

pISSN:

2309-4524

DOI:

10.34028/iajit

Concurrent system

maximality-based semantics

process algebra

model checking

CTL

Issues

Article Details

Using Maximality-Based Labeled Transition System Model for Concurrency Logic Verification

Authors: N. A.

Publisher: Zarqa University, Jordan

Journal: The International Arab Journal of Information Technology (IAJIT) Vol.2 Issue 3, pp.23-29

Document Type: Article

Publication Date: 1/2005

Document Language: English

Document ID (Org No.): 2001388717

pISSN: 2309-4524

DOI: 10.34028/iajit

Concurrent system

maximality-based semantics

process algebra

model checking

CTL

Issues

Authors:

N. A.

Publisher:

Zarqa University, Jordan

Journal:

The International Arab Journal of Information Technology (IAJIT) Vol.2 Issue 3, pp.23-29

Document Type:

Article

Publication Date:

1/2005

Document Language:

English

Document ID (Org No.):

2001388717

pISSN:

2309-4524

DOI:

10.34028/iajit