ACTLW - an action-based computation tree logic with unless operator

Robert Meolic (Avtor), Tatjana Kapus (Avtor), Zmago Brezočnik (Avtor)

Povzetek

Model checkers for systems represented by labelled transition systems are not as extensively used as those for systems represented by Kripke structures. This is partially due to the lack of an elegant formal language for property specification which would not be as raw as, for example, HML yet also not as complex as, for example, -calculus. This paper proposes a new action-based propositional branching-time temporal logic ACTLW, which enhances popular computation tree logic (CTL) with the notion of actions in a similar but more comprehensive way than action-based CTL introduced by De Nicola and Vaandrager [R. De Nicola, F.W. Vaandrager, Action versus logics for transition systems, in: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, 1990, pp. 407-419]. ACTLW is defined by using temporal operators until and unless only, whereas all other temporal operators are derived from them. Fixed-point characterisation of the operators together with symbolic algorithms for globalmodel checking are shown. Usage of this new logic is illustrated by an example of verification of mutual-exclusion algorithms.

Ključne besede

formalna verifikacija;model za preverjanje;algoritmi;formal verification;model checking;action-based temporal logic;fixed point;mutual-exclusion algorithm;

Podatki

Jezik:	Angleški jezik
Leto izida:	2008
Tipologija:	1.01 - Izvirni znanstveni članek
Organizacija:	UM FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
UDK:	004.92
COBISS:	12047638
ISSN:	0020-0255
Št. ogledov:	1766
Št. prenosov:	91
Ocena:	0 (0 glasov)
Metapodatki:

Ostali podatki

Sekundarni jezik:	Angleški jezik
Sekundarne ključne besede:	formalna verifikacija;model za preverjanje;algoritmi;
URN:	URN:SI:UM:
Strani:	str. 1542-1557
Letnik:	ǂVol. ǂ178
Zvezek:	ǂiss. ǂ6
Čas izdaje:	2008
ID:	8718602