Task 3.4

Modeling of existing systems as Mathematical Services

Last updated: 1 October 2004 by Marco Bozzano

See also Node report and Task 1.2 report

Technical Objective

Task 3.4 is part of the Task 3 (Case studies). It is described in the Calculemus network proposal as follows:

"Modeling of existing systems as Mathematical Services."

Deliverables

There is one deliverable for Task 3.4:

Milestone 3.2 [due after 42 months]. Modeling of existing systems as Mathematical Services

Partner nodes

The sites and researchers involved in this task are:

ITC-IRST, Trento (Leader of the task):
Gilles Audemard (young visiting researcher from University of Provence, France)
Piergiorgio Bertoli (researcher)
Marco Bozzano (researcher)
Alessandro Cimatti (researcher)
Tommi Junttila (young visiting researcher from Helsinki University of Technology, Finland)
Gavin Keighren (young visiting researcher from University of Edumburgh, Scotland)
Veselin Kirov (young visiting researcher from Bulgaria)
Artur Kornilowicz, (young visiting researcher from University of Bialystok, Poland)
Roberto Sebastiani (assistant professor)
Stephan Schulz (young visiting researcher visiting IRST, from TU Muenchen)
Daniel Sheridan (young visiting researcher from University of Edimburgh)
Peter van Rossum (young visiting researcher from the Netherlands)

University of Genova, Italy -- UNIGE:
Alessandro Armando (Assistant Professor)
Luca Compagna (PhD student)
Pasquale De Lucia (PhD Student)
Enrico Giunchiglia (Associate Professor)
Silvio Ranise (PhD Student)

University of Bialystok, Poland -- UWB:
Andrzej Trybulec (Full Professor)
Czeslaw Bylinski
Grzegorz Bancerek
Adam Grabowski
Adam Naumowicz
Artur Kornilowicz
Josef Urban (Young visiting researcher from Charles University, Czech Republic)

Active young visiting researchers in the task

Gilles Audemard (University of Provence). Young visiting researcher at IRST (Trento) from 11/01 to 11/02.

Gilles' work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving & computing services) and logical reasoning capabilities (proving services), with the main goal of automatically verifying timed systems. In particular, he takes part to the requirement analysis, design and implementation of MathSAT [4], a system combining the (high-performances) boolean reasoning capabilities of the SAT procedure SIM with the mathematical solving capability of a home-made decision procedure for linear arithmetic formulas over the reals. He has taken in charge the development of the resulting system.
He contributed to the development of the general framework (logical foundations and basic algorithms) for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [3]. To this extent, his contribution focused mainly on the requirements for boolean decision procedures.

Luca Compagna (University of Genova). Young visiting researcher of UED (Edinburgh) from 07/01 to 08/01.

Luca's work focussed on the design, development, and efficient integration of decision procedures in formula simplification. He has contributed to the development of the RDL theorem prover.

Artur Kornilowicz (University of Bialystok). Young visiting researcher at IRST (Trento) from 07/01 to 06/02.

Artur's work focuses on the design and implementation of efficient algorithms that automatically establish the satisfiability of a specific class of mathematical formulae, which can be used to model timed systems. The algorithms are designed in order to closely integrate as a Math-Solver module of MathSAT [4]. He has taken in charge the development of the Math-Solver module.
He contributed too to the development of the general framework for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [3]. To this extent, his contribution focused mainly on the the requirements for mathematical solvers.

Silvio Ranise (University of Genova). Young visiting researcher of USAAR (Saarbruecken) from 11/01 to 12/01.

Silvio has actively participated in the definition of the control component of OMRS (Open Mechanized Reasoning Systems). Silvio's work focused also on the definition of Constraint Contextual Rewriting. He has contributed to the development of the RDL theorem prover.

Josef Urban (Charles University). Young visiting researcher at University of Bialystok from 02/02 to 08/02.

Josef's work consisted on designing an XML format for the Mizar system, that would enable various presentation and export functions for the Mizar Mathematical Library. Another task was to explore the Mizar type system and formalize related type theories in Mizar.

Daniel Sheridan (School of Informatics, University of Edumburgh). Young visiting researcher of IRST (Trento) from 13/2/03 to 6/4/03.

Daniel's work focussed in improved bounded model checking encodings, by reasoning about temporal logic as well as the problem domain in general, in particular the use of techniques from temporal logic theorem proving; and generally increasing the applicability of bounded model checking. His work at ITC-IRST was concerned with both the symbolic and bounded model checking aspects of the NuSMV model checker: improving the behaviour of the system on non-Boolean data types and integrating the improved encoding routines that were the results of his research.

Veselin Kirov (Bulgaria). Young visiting researcher of IRST (Trento) from 1/6/03 to 31/10/03 and from 1/3/04 to 30/4/04.

Stephan Schulz (TU Muenchen). Young visiting researcher at RISC, visiting IRST (Trento) from 7/1/2004 to 26/3/04.

Stephan worked on four main topics during his CALCULEMUS stay: Communication protocols for reasoning systems, improvements for first-order deduction systems, automated domain exploration, and decision procedures for fragments of first order logic. Most of his work at ICT/irst was on the last topic. He developed and implemented a robust and efficient congruence closure algorithm that forms the equational solver of the latest version of MathSat. The system makes MathSat into an efficient decision procedure for the logic of equality with uninterpreted function symbols (EUF) and plays an important role in reasoning about other theories. In fall 2003, Stephan attended the Fourth International Workshop on the Implementation of Logics (as an invited speaker) and LPAR-2004. In summer 2004, he presented a number of results obtained during his CALCULEMUS work at IJCAR-2004 and the IJCAR-Workshop on Empirically Successful First-Order Reasoning. He published the papers [14,15,16,17].

Tommi Junttila (Helsinki University of Technology, Finland). Young visiting researcher of IRST (Trento) from 15/1/04 to 31/8/04.

Tommi's work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving) and logical reasoning capabilities (proving services). In particular, he took part to the requirement analysis, design and implementation of the new version of MathSAT [4], a system combining the (high-performance) boolean reasoning capabilities with the mathematical solving capability. His main contributions were the designing and implementing the top-level solver module and the preprocessor for non-clausal formulae in the new version of the MathSAT solver. The top-level solver extends the Minisat Boolean satisfiability checker developed at Chalmers University by interfacing it with the data structures representing non-Boolean formulae and with theory specific solvers such as one for the theory of equality with uninterpreted functions and one for linear and non-linear arithmetics. The preprocessor for non-clausal formulae enables one to use more natural and compact form for describing problems. The formulae are then translated to the special conjunctive normal form accepted by the top-level solver by a series of satisfiability preserving steps. In addition, he has contributed to the bounded model checker module of the NuSMV symbolic model checker. He has improved the Boolean circuit package in NuSMV so that it now produces more compact representations of problems. Furthermore, he has designed and implemented a module for incremental satisfiability checking in NuSMV. Based on this module, he has implemented the temporal induction algorithms described by Een and Sorensen in [9] and integrated incremental SAT solving also to bounded model checking of linear time temporal properties. During his stay in Trento he has participated in two conferences, the International Conference on Application of Concurrency to System Design (ACSD 2004) in Hamilton, Canada, June 2004 and 25th International Conference on Application and Theory of Petri Nets (ATPN 2004) in Bologna, Italy, June 2004. In these conferences, he presented new results concerning the symmetry reduction method for explicit state space anylysis obtained prior to the visit at IRST. The presented papers are [10][11] The conference trips were funded by IRST through the CALCULEMUS project.

Peter van Rossum (The Netherlands). Young visiting researcher of IRST (Trento) from 15/1/04 to 31/8/04.

Gavin Keighren (University of Edumburgh). Young visiting researcher at IRST (Trento) from 1/3/04 to 31/8/04.

The focus of his work has been towards the constant improvement of the model checker NuSMV. Initially this involved working on increasing the functionality provided by the program, by means of allowing input files to be automatically run through external preprocessors. He also made the modifications necessary to integrate the improved RBC encodings which Tommi Junttila had provided. He has been involved in the revision of the user-manual and tutorial to reflect the changes made to NuSMV. The other main area of his work has been to investigate the boolean encoding methods used by NuSMV, with the aim of improving the solution times for SAT-based bounded model checking. Primarily, it has focused on reducing the size of the formula which is passed to the external SAT solver. He has also been involved in the testing and benchmarking of the new incremental algorithms which have been added to the latest version of NuSMV.

Report of current status of the task

UNIGE's contribution to the task consists of the rational reconstrution of the Maple evaluation process in terms of Constraint Contextual Rewring jointly done by Alessandro Armando (UNIGE) and Clemens Ballarin (UKA) (see [2]). Maple's evaluator, together with a feature that is usually known as the assume facility, is a combination of modules with specialised reasoning capabilities. These modules have been identified, their interfaces specified, and their interplay reconstructed as Constraint Contextual Rewriting (CCR), a powerful form of conditional rewriting that incorporates the services provided by a decision procedure. Finally it has been shown how Maple's evaluation process can be strengthened by borrowing ideas from CCR.

As ITC-IRST contribution to the task, we show how existing systems are captured by our framework described in task 1.2 [3]. In particular:

Omega (Program Verification) [Pugh 92]
SMV + QUAD-CLP (Program Verification) [Chan et al 97]
TSAT (Temporal Reasoning) [Armando et al 99]
LPSAT (Resource Planning) [Wolman and Weld 99]
MathSAT (Temporal Reasoning) [Audemard et al. 02]

Systems, software, or approaches

MathSAT proposed by IRST.
MathSAT is a decision procedures for combinations of boolean and linear mathematical propositions, based on two main ingredients. The first is a SAT procedure, for dealing efficiently with the propositional component of the problem. The second is a tight integration, within the DPLL architecture, of a set of mathematical deciders for theories of increasing expressive power. The existence of such procedure opens the ability to solve problems arising from real-world domains such as verification of timed and hybrid systems and planning with resources [12].
The ultimate goal is to design and implement a system which can verify real world systems and protocols, handling both the boolean reasoning component and the mathematical solving component of these problems. In particular, we focus on systems whose modeling involve time aspects. [4,5]
RDL proposed by UNIGE.
RDL is a system for formula simplification developed within the Constraint Contextual Rewriting Project. RDL is an acronym for Rewrite and Decision procedure Laboratory. The system allows for experimenting with the integration of decision procedures and conditional rewriting.
The Logic Broker Architecture proposed by UNIGE.
LBA is a framework which provides the needed infrastructure for making mechanized reasoning systems interoperate (see [6]). The architecture provides location transparency, a way to forward requests for logical services to appropriate reasoning systems via a simple registration/subscription mechanism, and a translation mechanism which ensures the transparent and provably sound exchange of logical services.

Publications and References

1: R. Sebastiani.
Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms.
ITC-IRST Technical report 0111-22. November 2001.
2: A. Armando and C. Ballarin.
Maple's Evaluation Process as Constraint Contextual Rewriting.
In the Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC'2001). July 22 - 25, 2001, ORCCA and University of Western Ontario.
3: G. Audemard, P.Bertoli, A. Cimatti, A.Kornilowicz and R. Sebastiani.
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms and Requirements.
In Artificial Intelligence and Symbolic Computation. Proc. of Joint AISC 2002 and CALCULEMUS 2002. Marseille, France, July 1-5 2002. LNAI N.2385 © Springer Verlag.
4: G. Audemard, P.Bertoli, A. Cimatti, A.Kornilowicz and R. Sebastiani.
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.
In Proc. 18th Int. Conference on Automated Deduction (CADE-18), part of Federated Logic Conference (FLoC'02). Copenhagen, Denmark, July 2002. LNAI N.2392 © Springer Verlag.
5: G. Audemard, A. Cimatti, A. Kornilowicz and R. Sebastiani.
Bounded Model Checking for Timed Systems.
In Proc. 22nd Joint International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002). Houston, TX, USA, November 2002. LNCS © Springer Verlag (to appear).
6: A. Armando, L. Compagna, and S. Ranise.
System Description: RDL---Rewrite and Decision procedure Laboratory
In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001), June 18-23, 2001, Siena, Italy. © Springer-Verlag
7: A. Armando, L. Compagna, S. Ranise.
Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation.
In Festschrift in Honor of Jörg H. Siekmann. To appear in Lecture Notes in Artificial Intelligence, © Springer Verlag.
8: A. Armando, C. Castellini, E. Giunchiglia, F. Giunchiglia, A. Tacchella.
SAT-Based Decision Procedures for Automated Reasoning: a Unifying Perspective.
In Festschrift in Honor of Jörg H. Siekmann. To appear in Lecture Notes in Artificial Intelligence, © Springer Verlag.

9: Niklas Eén and Niklas Sörensson.; Temporal induction by incremental SAT solving.
Electronic Notes in Theoretical Computer Science, 89(4).
Elsevier, 2004.
10: Tommi Junttila.; New Orbit Algorithms for Data Symmetries.
In "Proc. Application of Concurrency to System Design 2004", pages 175-184.
IEEE, 2004.
11: Tommi Junttila.; New Canonical Representative Marking Algorithms for Place/Transition-Nets.
In "Proc. Application and Theory of Petri Nets 2004", pages 258-277.
LNCS 3099. Springer, 2004.
12: G. Audemard, M.Bozzano, A.Cimatti and R.Sebastiani.
Verifying Industrial Hybrid Systems with MathSat.
In Proc. PDPAR 2003. Miami, Florida, July 29, 2003.

13: M.Bozzano, A.Cimatti, G.Colombini, V.Kirov and R.Sebastiani.
The MathSat solver -- a progress report.; In Proc. PDPAR 2004, Cork, Ireland, July 5, 2004.

14: S. Sutcliffe and S. Schulz and T. Tammet (eds).; Proceedings of the IJCAR Workshop on Empirically Successful First Order Reasoning (ESFOR-2004), Cork, Ireland.
ENTCS, Elsevier Science, 2004.
15: S. Sutcliffe and J. Zimmer and S. Schulz.; TSTP Data-Exchange Formats for Automated Theorem Proving Tools.
In V. Sorge and W. Zhang (eds.): Distributed and Multi-Agent Reasoning, Frontiers and Artificial Intelligence and Application.
IOS Press, 2004
16: S. Schulz.; System Description: E 0.81.
In D. Basin and M. Rusinowitch (eds.): Proc. of the 2nd IJCAR, Cork, Ireland.
LNAI 3097, Springer, 2004.
17: S. Schulz.; Simple and Efficient Clause Subsumption with Feature Vector Indexing.
In G. Sutcliffe and S. Schulz and T. Tammet (eds.): Proc. of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving, Cork, Ireland.
ENTCS, Elsevier Science, 2004.

Task 3.4 Modeling of existing systems as Mathematical Services

Official Start and End