Temporal logics are well suited for reasoning about actions, as they allow for the specification of domain descriptions including temporal constraints as well as for the verification of temporal properties. The article deals with verification of action theories defined in a temporal extension of answer set programming which combines ASP with a dynamic linear time temporal logic (DLTL). The article proposes an approach to bounded model checking that exploits the Büchi automaton construction while searching for a counterexample, with the aim of achieving completeness. The article provides an encoding in ASP of the temporal action domains and of Bounded Model Checking of DLTL formulas. The article also deals with reasoning about epistemic knowledge and incomplete states.

The verification of compliance of business processes to norms requires the representation of different kinds of obligations, including achievement obligations, maintenance obligations, obligations with deadlines and contrary to duty obligations. In this paper we develop a deontic temporal extension of Answer Set Programming (ASP) suitable for verifying compliance of a business process to norms involving such different types of obligations. To this end, we extend Dynamic Linear Time Temporal Logic (DLTL) with deontic modalities to define a Deontic DLTL. We then combine it with ASP to define a deontic action language in which until formulas and next formulas are allowed to occur within deontic modalities. We show that in the language we can model the different kinds of obligations which are useful in the verification of compliance to normative requirements. The verification can be performed by bounded model checking techniques.

Abstract In this paper, we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.

Abstract The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent annotations as well as data awareness in a uniform way. It allows for a declarative specification of a business process but also for encoding processes specified in conventional workflow languages. Verification of temporal properties of a business process, including verification of compliance to business rules, is performed by bounded model checking techniques in Answer Set Programming, extended with constraint solving for dealing with conditions on numeric data.

The paper defines a notion of conformance of a set of k agents with a multiparty protocol with k roles, requiring the agents to be interoperable and to produce correct executions of the protocol. Conditions are introduced that enable each agent to be independently verified with respect to the protocol.

We present a tableau-based algorithm for obtaining a Buchi automaton from a formula in dynamic linear time temporal logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Buchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton.

The paper presents a logic for action theory based on a modal language, where modalities represent actions. The frame problem is tackled by using a nonmonotonic formalism which maximizes persistency assumptions. The problem of ramification is tackled by introducing a modal causality operator which is used to represent causal rules. Assumptions on the value of fluents in the initial state allow reasoning with incomplete initial states and postdiction. The action theory can also deal with nonminimal change and nondeterministic actions.

In this paper we present a modal extension of logic programming, which allows both multiple universal modal operators and embedded implications. We show that this extension is well suited for structuring knowledge and, more specifically, for defining module constructs within programs, for representing agents beliefs, and also for hypothetical reasoning. The language contains modalities [a1] to represent agent beliefs, and a modality □ which is a kind of common knowledge operator. It allows sequences of modalities to occur in front of clauses, goals and clause heads, and hypothetical implications to occur in goals and in clause bodies. We present a goal directed proof procedure for the language, and several examples of its use for defining modules are given. In particular, the language allows different proposals to be captured for module definition and composition presented in the literature. The modal logic, of which our programming language is a clausal fragment, is introduced through its Kripke semantics. This has strong similarities with the possible world semantics for the (propositional) logics of knowledge and belief proposed by Halpern & Moses. A cut-free sequent calculus is also given for this logic, which proves the soundness and completeness of the goal-directed proof procedure by showing that goal directed proofs correspond to some sequent proofs.

In this paper we present various logical characterizations of justification‐based (nonmonotonic) truth maintenance systems (JTMS). These characterizations, which are proved to be equivalent, aim at describing dependency‐directed backtracking (DDB) (i.e., the process of resolving conflicts which can arise when nogoods are allowed in the set of justifications), mainly relying on the intuitive idea that a contrapositrve use of justifications is needed to resolve inconsistencies. The idea is first formalized by means of the notion of three‐valued labeling and then through a transformation which explicitly adds all contrapositives of the justifications. An abductive characterization of the JTMS is provided through a further transformation which converts a set of nonmonotonic justifications to a corresponding abduction framework. This approach provides a unifying framework, based on the notion of abduction, for describing both JTMSs and assumption‐based TMSs (ATMSs).

The unification problem in f'mst-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given.A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given.A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases.

Finding the solution of a dynamic programming problem m the form of polyadlc funcUonal equatmns is shown to be equivalent to searching a mmmaal cost path in an AND/OR graph with monotone cost functions The proof is given in an algebraic framework and is based on a commutaUvity result between solutton and mterpretauon of a symbohc system This approach Is simdar to the one used by some authors to prove the eqmvalence between the operaUonal and denotatmnal semantics of programming languages

By defining a suitable algebra for cut sets, it is possible to reduce the problem of enumerating the cut sets between all pairs of nodes in a graph to the problem of solving a system of linear equations. An algorithm for solving this system using Gaussian elimination is presented in this paper. The efficiency of the algorithm depends on the implementation of sum and multiplication. Therefore, some properties of cut sets are investigated, which greatly simplify the implementation of these operations for the case of undirected graphs. The time required by the algorithm is shown to be linear with the number of cut sets for complete graphs. Some experimental results are given, proving that the efficiency of the algorithm increases by increasing the number of pairs of nodes for which the cut sets are computed.