Deductive temporal reasoning with constraints

Dixon, Clare ORCID: 0000-0002-4610-9533, Konev, Boris ORCID: 0000-0002-6507-0494, Fisher, Michael and Nietiadi, Sherly (2013) Deductive temporal reasoning with constraints. JOURNAL OF APPLIED LOGIC, 11 (1). pp. 30-51.

Text jal12updated.pdf - Author Accepted Manuscript Download (433kB)

Abstract

When modelling realistic systems, physical constraints on the resources available are often required. For example, we might say that at most N processes can access a particular resource at any moment, exactly M participants are needed for an agreement, or an agent can be in exactly one mode at any moment. Such situations are concisely modelled where literals are constrained such that at most N, or exactly M, can hold at any moment in time. In this paper we consider a logic which is a combination of standard propositional linear time temporal logic with cardinality constraints restricting the numbers of literals that can be satisfied at any moment in time. We present the logic and show how to represent a number of case studies using this logic. We propose a tableau-like algorithm for checking the satisfiability of formulae in this logic, provide details of a prototype implementation and present experimental results using the prover. © 2012 Elsevier B.V. All rights reserved.

Item Type:	Article
Additional Information:	## TULIP Type: Articles/Papers (Journal) ##
Uncontrolled Keywords:	Temporal logic, Constraints, Theorem proving, Tableau
Depositing User:	Symplectic Admin
Date Deposited:	06 Jul 2017 13:06
Last Modified:	19 Jan 2023 07:00
DOI:	10.1016/j.jal.2012.07.001
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3008352