25th International Symposium on Temporal Representation and Reasoning (TIME 2018)Warsaw, Poland 15-17 October 2018.
Autores: Alexander Bolotov / Montserrat Hermo / Paqui Lucio /
Palabras Clave: Branching Temporal Logic - Fairness Constraints - Model checking - One-Pass Tableau
We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a first-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.
Autores: Alex Abuin / Hubie Chen / Montserrat Hermo / Paqui Lucio /
Palabras Clave: Automatic verification - Dafny - inductive predicate - proof system - tractability results
In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.
Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio /
Palabras Clave: Model checking - SAT - SMT - Solvers - Tableux
When building tableau for temporal logic formulae, applying a two-pass con- struction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second ‘pass’, we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtain- ing a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.
Autores: Alex Abuin / Alexander Bolotov / Montserrat Hermo / Paqui Lucio /
Palabras Clave: branching-time - expressiveness - fairness - Temporal Logic
In this article we propose an automatic test generation technique for evaluating the implementation of a reactive system with respect to the set of requirements from which it has been developed. We consider reactive systems that interact with its environment via variables whose values (at each instant) depends on events or sensors. Our test cases are graphs that represent a collection of executions (or traces) of the system that captures all possible behaviours of the environment. Our proposal is a technique to automatically construct these graphs exploding the ability of model checkers to generate counter-examples for temporal properties that are not satisfied by a system model. Further work includes to implement a prototype for experimenting the technique on a test suite of industrial requirements, and also to design and implement some techniques to gain scalability.
Autores: Montserrat Hermo / Paqui Lucio / Josu Oca /
Palabras Clave: Model checking - Reactive Systems - Test Generation
Functional and multivalued dependencies play an important role in the design of relational databases. There is a strong connection between data dependencies and some fragments of the propositional logic. In particular, functional dependencies are closely related to Horn formulas. Also, multivalued dependencies are characterized in terms of multivalued formulas. It is known that both Horn formulas and sets of functional dependencies are efficiently learnable in the exact model of learning with queries. In this work, we study the learnability of a non-trivial subclass of multivalued formulas called CRMVDF. We use Angluin’s exact learning model with membership and equivalence queries and present a polynomial time algorithm which exactly learns CRMVDF from entailments.
Autores: Montserrat Hermo / Ana Ozaki /
Palabras Clave:
La referencia completa es:Abuin, A., Díaz de Cerio, U., Hermo, M. and Lucio, P., Verified Model Checking for Conjunctive Positive Logic. SN COMPUTER SCIENCE, VOL 2, Springer 2021. https://doi.org/10.1007/s42979-020-00417-3
Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio /
Palabras Clave: Conjunctive positive logic - Dafny - Model checking - proof system - Quantified constraint satisfaction problem - Verification