Title :
Parameterised Process Algebraic Verification by Precongruence Reduction
Author :
Siirtola, Antti ; Kortelainen, Juha
Author_Institution :
Dept. of Inf. Process. Sci., Univ. of Oulu, Oulu, Finland
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;
Conference_Titel :
Application of Concurrency to System Design, 2009. ACSD '09. Ninth International Conference on
Conference_Location :
Augsburg
Print_ISBN :
978-0-7695-3697-2
DOI :
10.1109/ACSD.2009.9
