| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Show document Help

Title:ACTLW - an action-based computation tree logic with unless operator
Authors:ID Meolic, Robert (Author)
ID Kapus, Tatjana (Author)
ID Brezočnik, Zmago (Author)
Files:URL http://dx.doi.org/10.1016/j.ins.2007.10.023
 
Language:English
Work type:Unknown
Typology:1.01 - Original Scientific Article
Organization:FERI - Faculty of Electrical Engineering and Computer Science
Abstract: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.
Keywords:formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Year of publishing:2008
PID:20.500.12556/DKUM-27412 New window
UDC:004.92
ISSN on article:0020-0255
COBISS.SI-ID:12047638 New window
NUK URN:URN:SI:UM:DK:3YIKV5KG
Publication date in DKUM:01.06.2012
Views:2512
Downloads:104
Metadata:XML DC-XML DC-RDF
Categories:Misc.
:
MEOLIC, Robert, KAPUS, Tatjana and BREZOČNIK, Zmago, 2008, ACTLW - an action-based computation tree logic with unless operator. Information sciences [online]. 2008. [Accessed 21 January 2025]. Retrieved from: http://dx.doi.org/10.1016/j.ins.2007.10.023
Copy citation
  
Average score:
0.5
1
1.5
2
2.5
3
3.5
4
4.5
5
(0 votes)
Your score:Voting is allowed only for logged in users.
Share:Bookmark and Share


Hover the mouse pointer over a document title to show the abstract or click on the title to get all document metadata.

Record is a part of a journal

Title:Information sciences
Shortened title:Inf. sci.
Publisher:North-Holland
ISSN:0020-0255
COBISS.SI-ID:25613056 New window

Secondary language

Language:English
Keywords:formalna verifikacija, model za preverjanje, algoritmi


Comments

Leave comment

You must log in to leave a comment.

Comments (0)
0 - 0 / 0
 
There are no comments!

Back
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica