The paper presents a novel SMT-based method for testing the satisfiability of formulae that express strategic properties of timed multi-agent systems represented by networks of timed automata. Strategic Metric Temporal Logic (SMTL) is introduced, which extends Metric Temporal Logic (MTL) with strategy operators. SMTL is interpreted over maximal continuous time runs of timed automata. We define a procedure that synthesises a model for a given SMTL formula if such a model exists. The method exploits Satisfiability Modulo Theories (SMT) techniques and Parametric Bounded Model Checking algorithms. The presented approach enables bounded satisfiability checking, where the model is partially given and needs to be completed in line with the given specification. Our method has been implemented, and its application is demonstrated through an example of the well-known dining philosophers problem extended with clocks and strategies. The experimental results are quite encouraging.

In this paper, we introduce a new method of the satisfiability (SAT) checking for Simple-Goal Strategy Logic (SL[SG]), using symbolic Boolean model encoding and the SAT Modulo Monotonic Theories techniques, which was implemented into the tool SGSAT. To the best of our knowledge, this is the only tool solving the SAT problem for SL[SG]. Its applications include process synthesis, developing controllers as well as automatic planners in multi-agent scenarios.

Synthesis of models and strategies is a very important task in software engineering. The main problem here consists in checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a novel method for deciding the satisfiability of formulae of Alternating-time Temporal Logic (ATL) under perfect and imperfect information. The synthesised models of strategic games are often minimal. The method expands the one for CTL exploiting SAT Modulo Monotonic Theories (SMMT) solvers. Our tool MsATL combines SMMT solvers with two existing ATL model checkers: MCMAS and STV. This is the first ever tool for checking the satisfiability of imperfect information ATL. The experimental results show that, similarly to the CTL case, our approach appears to be very efficient and can quickly check the satisfiability of large ATL formulae that have been out of reach of the existing approaches.

We present nine SAT-solvers and compare their efficiency for several decision and combinatorial problems: three classical NP-complete problems of the graph theory, bounded Post correspondence problem (BPCP), extended string correction problem (ESCP), two popular chess problems, PSPACE-complete veri fication of UML systems, and the Towers of Hanoi (ToH) of exponential solutions. In addition to several known reductions to SAT for the problems of graph k-colouring, vertex k-cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, and ToH, SCP, and BPCP. Our extensive experimental results allow for drawing quite interesting conclusions on efficiency and applicability of SAT-solvers to different problems: they behave quite efficiently for NP-complete and harder problems but they are by far inferior to tailored algorithms for specific problems of lower complexity.

We present the web service composition system TripICS, which allows for an easy and user-friendly planning of visits to interesting cities and places around the world in combination with travels, arranged in the way satisfying the user’s requirements. TripICS is a specialization of the concrete pla nning of PlanICS viewed as a constrained optimization problem to the ontology containing services provided by hotels, airlines, railways, museums etc. The system finds an optimal plan by applying a modification of the most efficient concrete planner of PlanICS based on a combination of an SMT-solver with the algorithm GEO. The modification has been designed in order to solve quickly multiple equality constraints. The efficiency of the new planning algorithm is proved by experimental results.

The paper deals with the concrete planning problem – a stage of the web service composition in the PlanICS framework. We present several known and new methods of concrete planning including those based on Satisfiability Modulo Theories (SMT), Genetic Algorithm (GA), as well as methods combining SMT with GA and other nature-inspired algorithms such as Simulated Annealing (SA) and Generalised Extremal Optimization (GEO). The discussion of all the approaches is supported by the complexity analysis, extensive experimental results, and illustrated by a running example.

The paper deals with the concrete planning problem (CPP) – a stage of the Web Service Composition (WSC) in the PlanICS framework. The complexity of the problem is discussed. A novel SMT-based approach to CPP is defined and its performance is compared to the standard Genetic Algorithm (GA) and the OpenOpt numerical toolset planner in the framework of the PlanICS system. The discussion of all the approaches is supported by extensive experimental results.

Automating the composition of web services is an object of a growing interest. In our paper [13] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this composition aimed at building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments.

The paper presents a prototype toolset to planning by automatic composition of web services. The main idea consists in arranging the composition into two main phases: abstract and concrete one, as well as to handle fully declarative user queries. The

The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the (prototype) tool BMC4UML and some experimental results are presented.