INFORMATION CONTROL NETS AS PROCESSES - QUALITATIVE-ANALYSIS

In this paper, we address the formal verification in workflow systems. More precisely, we consider the automatic verification of one of the most prominent workflow low models, namely the Information Control Net s (ICNs) model. We present a powerful method for the qualitative analy sis of ICNs. The analysis proposed rests on an observed analogy betwee n ICNs and usual process algebra. Actually, ICNs are translated into C CS process algebra agents. The properties to be verified are expressed in a temporal logic, the propositional modal nu-calculus. The verific ation is done thanks to model-checking algorithms.