| | SLO | ENG | Piškotki in zasebnost

Večja pisava | Manjša pisava

Izpis gradiva Pomoč

Naslov:ACTLW - an action-based computation tree logic with unless operator
Avtorji:ID Meolic, Robert (Avtor)
ID Kapus, Tatjana (Avtor)
ID Brezočnik, Zmago (Avtor)
Datoteke:URL http://dx.doi.org/10.1016/j.ins.2007.10.023
 
Jezik:Angleški jezik
Vrsta gradiva:Neznano
Tipologija:1.01 - Izvirni znanstveni članek
Organizacija:FERI - Fakulteta za elektrotehniko, računalništvo in informatiko
Opis: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:formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Leto izida:2008
PID:20.500.12556/DKUM-27412 Novo okno
UDK:004.92
COBISS.SI-ID:12047638 Novo okno
ISSN pri članku:0020-0255
NUK URN:URN:SI:UM:DK:3YIKV5KG
Datum objave v DKUM:01.06.2012
Število ogledov:2512
Število prenosov:104
Metapodatki:XML DC-XML DC-RDF
Področja:Ostalo
:
Kopiraj citat
  
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
Objavi na:Bookmark and Share


Postavite miškin kazalec na naslov za izpis povzetka. Klik na naslov izpiše podrobnosti ali sproži prenos.

Gradivo je del revije

Naslov:Information sciences
Skrajšan naslov:Inf. sci.
Založnik:North-Holland
ISSN:0020-0255
COBISS.SI-ID:25613056 Novo okno

Sekundarni jezik

Jezik:Angleški jezik
Ključne besede:formalna verifikacija, model za preverjanje, algoritmi


Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj
Logotipi partnerjev Univerza v Mariboru Univerza v Ljubljani Univerza na Primorskem Univerza v Novi Gorici