Parameterised Process Algebraic Verification by Precongruence Reduction

Author

Siirtola, Antti ; Kortelainen, Juha

Author_Institution

Dept. of Inf. Process. Sci., Univ. of Oulu, Oulu, Finland

fYear

2009

fDate

1-3 July 2009

Firstpage

158

Lastpage

167

Abstract

Decidability of the parameterised verification problem is shown for a class of systems and safety properties given as (multiply) parameterised labelled transition systems with an (infinite) set of valuations representing the allowed parameter values. The idea is to reduce the set of valuations by exploiting the precongruence of the correctness relation (traces refinement). An algorithm based on the result is provided.

Keywords

Petri nets; decidability; finite state machines; formal specification; process algebra; program diagnostics; program verification; set theory; correctness relation; decidability problem; infinite valuation set; parameterised finite-state machine; parameterised labelled transition system; parameterised process algebraic verification problem; precongruence reduction; safety property; specification-system LTS pair; trace refinement; Application software; Computational modeling; Concurrent computing; Cost accounting; Information processing; Safety; Topology; parameterised verification; process algebra; refinement checking;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 2009. ACSD '09. Ninth International Conference on

Conference_Location

Augsburg

ISSN

1550-4808

Print_ISBN

978-0-7695-3697-2

Type

conf

DOI

10.1109/ACSD.2009.9

Filename

5291049