Paper Info
Title
Structured Counterexamples for the Temporal Description Logic ALCCTL
Abstract
A new algorithm for generating counterexamples for the temporal description logic ALCCTL is presented. ALCCTL is a decidable combination of the description logic ALC and computation tree logic CTL. It extends CTL by first order quantified expressions over unary and binary predicates. Predicates and quantified expressions are required for representing properties in application domains such as structured web documents and they are frequently used in software and hardware specifications which are verified by model checking. In the case of a specification violation, existing algorithms generate counterexamples that tend to be complex yet imprecise if specifications range over sets of objects. The presented algorithm is the first algorithm for generating counterexamples for a temporal description logic that considers first order predicates and quantification. The algorithm is sound and semi-complete for ALCCTL. The generated counterexamples are both more precise and comprehensible than counterexamples generated by the previous algorithms.
Year
DOI
Venue
2010
10.1109/SEFM.2010.36
Software Engineering and Formal Methods
Keywords
Field
DocType
description logic alc,computation tree logic,model checking,structured counterexamples,decidable combination,order predicate,binary predicate,hardware specification,new algorithm,temporal description logic,temporal description logic alcctl,previous algorithm,computational modeling,binary trees,web pages,first order,temporal logic,ctl,description logic,semantics,counterexamples
Computation tree logic,Model checking,Programming language,Expression (mathematics),Unary operation,Computer science,Description logic,Binary tree,Theoretical computer science,Decidability,Temporal logic
Conference
ISBN
Citations 
PageRank 
978-1-4244-8289-4
5
0.47
References 
Authors
15
3
Name
Order
Citations
PageRank
Franz Weitl1295.70
Shin Nakajima2111.72
Burkhard Freitag325282.44