Search

We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based language based on relational updates rules that has been applied to specify topology-sensitive distributed protocols with asynchronous communication. In this setting, the absence of protocol anomalies can be reduced to a coverability problem in which the initial set of configurations is not fixed a priori (Existential Coverability Problem). Existential Coverability in GLog can naturally be expressed into Parameterized Verification judgements in Cubicle. The encoding is based on a translation of relational update rules into transition rules that modify cells of unbounded arrays. To show the effectiveness of the approach, we discuss several verification problems for distributed protocols and distributed objects, a challenging task for traditional verification tools. The experimental results show the flexibility and robustness of Cubicle for the considered class of protocol examples. [ABSTRACT FROM AUTHOR]

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic ℒ〈4LQSR,×〉(D) ( ℒ D 4 , × , for short). Our application solves the main TBox and ABox reasoning problems for ℒ D 4 , × . In particular, it solves the consistency and the classification problems for ℒ D 4 , × -knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports ℒ D 4 , × -knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language). [ABSTRACT FROM AUTHOR]

Extracting association rules from large datasets has been widely studied in many variants in the last two decades; they allow to extract relations between values that occur more "often" in a database. With temporal association rules the concept has been declined to temporal databases. In this context the "most frequent" patterns of evolution of one or more attribute values are extracted. In the temporal setting, especially where the interference betweeen temporal patterns cannot be neglected (e.g., in medical domains), there may be the case that we are looking for a set of temporal association rules for which a "significant" portion of the original database represents a consistent model for all of them. In this work, we introduce a simple and intuitive form for temporal association rules, called pure evolving association rules (PE-ARs for short), and we study the complexity of checking a set of PE-ARs over an instance of a temporal relation under approximation (i.e., a percentage of tuples that may be deleted from the original relation). As a by-product of our study we address the complexity class for a general problem on Directed Acyclic Graphs which is theoretically interesting per se. [ABSTRACT FROM AUTHOR]

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic ℒ〈4LQSR,×〉(D) ( ℒ D 4 , × , for short). Our application solves the main TBox and ABox reasoning problems for ℒ D 4 , × . In particular, it solves the consistency and the classification problems for ℒ D 4 , × -knowledge bases represented in set-theoretic terms, and a generalization of the Conjunctive Query Answering problem in which conjunctive queries with variables of three sorts are admitted. The reasoner, which extends and improves a previous version, is implemented in C++. It supports ℒ D 4 , × -knowledge bases serialized in the OWL/XML format and it admits also rules expressed in SWRL (Semantic Web Rule Language). [ABSTRACT FROM AUTHOR]