Clare Dixon: PhD Projects 2014-15


Theorem Proving for Action Logics

(With Ullrich Hustadt)

In the logic and Computation Group we have developed resolution calculi and implemented theorem provers for a variety of non-classical logics. In particular, a resolution calculus for propositional linear time temporal logics has been developed in [1] and implemented in the theorem prover TRP++ [2], calculi for first-order temporal logics have been developed in [3,4] and this has been implemented in the provers TeMP [5] and TSPASS [6], and calculi for the branching-time temporal logic CTL have been developed in [7,8] and implemented in the prover CTL-RP [9]. The above all have a similar underlying structure. A formula is translated into a suitable normal form, known as clauses, often representing conditions on the initial state, conditions on the next moment in time and constraints that must be eventually satisfied. The normal form has the property that the original formula is satisfiable if and only if the transformed formula is satisfiable. Next, a series of resolution rules are applied which add new clauses to the clause set. Many of these are closely related to the binary resolution rule of classical propositional logic (see for example [10]). If false is detected then the set of clauses is unsatisfiable or if no new clauses can be derived then the set of clauses is satisfiable.

This project involves the extension of this approach to logics involving actions, in particular either Propositional Dynamic Logic[11] or Dynamic Linear Time Temporal Logic[12]. The former is a well studied logic where underlying models involves sets of states where propositional variables may be true or false, with relations between the states indexed by atomic actions. Formulae can be constructed from propositional connectives but can also involve action terms for example:

Action operators allowing sequential composition, non-deterministic choice etc can be used to construct complex action terms.

Dynamic Linear Time Temporal Logic[12] is a logic which extends linear time temporal logics with actions. It has been used to specify interaction protocols and web services[13,14] and has tableau decision procedure[12].

This project involves the development of a resolution style calculus for one or more of these logics involving the proposal of, and translation into, a suitable normal form, ideally involving only atomic actions and the development of resolution rules which can be applied to this normal form. The resulting calculus will need to be shown sound, complete and terminating and an implementation developed. Throughout the project, examples, and case studies will be collected and used to experiment with the developed prover.

References

[1] Fisher, M., Dixon, C., and Peim, M. Clausal Temporal Resolution, ACM Transactions on Computational Logic, volume 2, number 1, January 2001

[2] B. Konev, TRP++ Temporal Resolution Prover, http://www.csc.liv.ac.uk/%7Ekonev/software/trp++/

[3] Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. Mechanizing First-Order Temporal Resolution. Information and Computation 199(1-2):55-86. Elsevier Science, 2005.

[4] Degtyarev, A., Fisher, M., and Konev, B. Monodic Temporal Resolution. ACM Transactions on Computational Logic 7(1):108-150. ACM, January 2006.

[5] B. Konev, TeMP a Temporal Monodic Prover http://www.csc.liv.ac.uk/%7Ekonev/software/TeMP/

[6] M. Ludwig, TSPASS a fair monodic first-order temporal prover http://www.csc.liv.ac.uk/~michel/software/tspass/

[7] Bolotov, A., and Fisher M., A Clausal Resolution Method for CTL Branching Time Temporal Logic. Journal of Experimental and Theoretical Artificial Intelligence, volume 11, 1999, pages 77-93, Taylor & Francis.

[8] L. Zhang, U. Hustadt and C. Dixon First-order Resolution for CTL, University of Liverpool, Technical Report Series, Number ULCS-08-010

[9] L. Zhang CTL-RP http://www.csc.liv.ac.uk/%7Elan/softwares.html

[10] J. Kelly, The Essence of Logic, Prentice Hall 1997.

[11] D Harel, D. Kozen and J. Tiuryn, Dynamic Logic, MIT Press, 2000.

[12] L. Giordano and A. Martelli: Tableau-based automata construction for dynamic linear time temporal logic. Annals of Mathematics and Artificial Intelligence 46(3):289-315, 2006.

[13] L. Giordanoa and A. Martelli and Camilla Schwind: Specifying and verifying interaction protocols in a temporal action logic. Journal of Applied Logic 5(2):214-234, 2007.

[14] A. Martelli and L. Giordano: Reasoning about web services in a temporal action logic. In O. Stock and M. Schaerf, editors, Reasoning, Action and Interaction in AI Theories and Systems: Essays dedicated to Luigia Carlucci Aiello. LNCS 4155, pp. 229-246. Springer, 2006.

Verification of Robot Swarms

(With Michael Fisher)

Robot swarms are collections of, often simple, robots usually with some task to perform. In collaboration with Bristol Robotics Lab[20], in [21] we specified a swarm of robots each with a simple control mechanism known as the alpha algorithm. Each robot can sense nearby robots, can move forward, or make a turn if the robots it can sense fall below a certain threshold, or make a random turn. This alpha algorithm doesn't depend on any form of centralised control and utilises local wireless connectivity to detect nearby robots. Other, more sophisticated algorithms have been developed[22, 22a]. It is useful to be able to show that these algorithms really do result in the robots remaining as a coherent swarm, i.e. some robots don't move away from the main swarm and lose contact with them. However such environments are complex to model requiring a large number of robots, the location of the robots etc. and some thought will need to go into how these are modelled, so that provers and model checkers can cope with the specifications.

In [22b,22c] we apply model checking tools to prove properties of the alpha algorithm. We represent the movement area as a grid, consider several different types of concurrency, and vary both the wireless range and the alpha parameter. As the state spaces involved are large we can only model check small numbers of robots and small grid sizes, although the latter can be used to represent larger grids. The failing traces confirm the curvertex problem described in [22a].

Further, in [23] the authors consider a swarm of foraging robots. The robots aim to find and collect food and bring it back to the nest. Searching for food uses energy whereas bringing food back to the nest produces energy for the swarm. The underlying behaviour of these robots is represented by a transition systems where states represent the robot resting, leaving home, performing a random walk, scanning the arena for food, moving towards food etc. In [24] we have specified the underlying behaviour of the foraging swarm and using the provers TRP++[25] and TSPASS[26] proved certain properties.

This project involves developing reasoning techniques applicable to robot swarms. Initially a number of different swarm algorithms will be collected and their key features identified. Suitable formalisms will be investigated to represent these features, probably based on temporal logic. Tools, such as theorem provers[25,26,27] or model checkers[28], will be applied to the specifications to ascertain the practicality of the approach. We anticipate that the development of appropriate abstractions and sophisticated representations to represent large numbers of robots and grid sizes will be necessary to combat the state explosion problem. Dependent on the preliminary findings, this project may involve the development of theorem provers to allow proofs in the chosen target language or the development of a robot specification language and translation into a suitable underlying logic (utilising existing available provers or model checkers).

References

[20] Bristol Robotics Lab -- http://www.brl.ac.uk

[21] Winfield, A. F. T., Sa, J., Fernandez Gago, M-C., Dixon, C., and Fisher, M. On Formal Specification of Emergent Behaviours in Swarm Robotic Systems. International Journal of Advanced Robotic Systems 2(4):363-370, December 2005.

[22] A. F. T. Winfield, W. Liu, J.n Nembrini and A. Martinoli Modelling a wireless connected swarm of mobile robots. Swarm Intelligence, 2(2-4):241-266, December 2008.

[22a] Nembrini, J.: Minimalist Coherent Swarming of Wireless Networked Autonomous Mobile Robots. Ph.D. thesis, University of the West of England (2005)

[22b]Dixon, C., Winfield , A.F.T., and Fisher, M., Towards Temporal Verification of Emergent Behaviours in Swarm Robotic Systems. in the Proceedings of the 12th Conference Towards Autonomous Robotic Systems. 31st August - 2nd September 2011, Sheffield, UK. LNCS, Springer

[22c]Dixon, C., Winfield , A.F.T., Fisher, M., and Zeng, C. Towards Temporal Verification of Swarm Robotic Systems. Robotics and Autonomous Systems, 60(11): 1429-1441, Elsevier, 2012

[23] Liu W, Winfield A, Sa J, Chen J and Dou L, Strategies for Energy Optimisation in a Swarm of Foraging Robots, in SAB'06 Swarm Robotics Workshop, eds. Sahin E, Spears W and Winfield AFT, Springer-Verlag, LNCS 4433, pp 14-26, 2007.

[24] A. Behdenna, C. Dixon, and M. Fisher. Deductive Verification of Simple Foraging Robotic Behaviours. International Journal of Intelligent Computing and Cybernetics, 2(4): 604-643, World Scientific, 2009

[25] B. Konev, TRP++ Temporal Resolution Prover, http://www.csc.liv.ac.uk/%7Ekonev/software/trp++/

[26] M. Ludwig, TSPASS a fair monodic first-order temporal prover http://www.csc.liv.ac.uk/~michel/software/tspass/

[27] B. Konev, TeMP a Temporal Monodic Prover http://www.csc.liv.ac.uk/%7Ekonev/software/TeMP/

[28] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.

Verification of Robot Swarms Incorporating Uncertainty

(With Michael Fisher)

Robot swarms are collections of, often simple, robots usually with some task to perform. In collaboration with Bristol Robotics Lab in [20, 21] we specified and verified a swarm of robots each with a simple control mechanism known as the alpha algorithm. Each robot can sense nearby robots, can move forward, or make a turn if the robots it can sense fall below a certain threshold, or make a random turn. This alpha algorithm doesn't depend on any form of centralised control and utilises local wireless connectivity to detect nearby robots. To carry out formal verification we use the model checker NuSMV. However we need to abstract away from many details to make a discrete and finite model but even so the state explosion problem means that we can only verify small robot swarms.

Another issue is the need to incorporate uncertain information, for example variability in the physical aspects of the robots eg sensors, motors, grippers. To deal with this we could use probabilitic information. In [23,24] the authors consider a swarm of foraging robots. The robots aim to find and collect food and bring it back to the nest. Searching for food uses energy whereas bringing food back to the nest produces energy for the swarm. The underlying behaviour of these robots is represented by a transition systems where states represent the robot resting, leaving home, performing a random walk, scanning the arena for food, moving towards food etc. In [22] we specified and verified a group of foraging robots from [23,24] using the underlying probabilistic model from [24]. We considered different ways of modelling the swarm using the product of the individual robot transition systems as well as a population model. We use the PRISM [25] model checker to confirm many of the results in[24].

This project involves developing, applying and analysing reasoning techniques applicable to uncertainty in robot swarms. A number of probabilistic swarm algorithms will be collected and key features identified. Suitable formalisms will be investigated to represent these features, probably based on temporal logic. Tools, such as theorem provers[26,27,28] or model checkers[25], will be applied to the specifications to ascertain the practicality of the approach. Appropriate abstractions and sophisticated representations will need to be developed to allow verification. Additionally the development or combination of existing tools may be required.

References

[20] Winfield, A. F. T., Sa, J., Fernandez Gago, M-C., Dixon, C., and Fisher, M. On Formal Specification of Emergent Behaviours in Swarm Robotic Systems. International Journal of Advanced Robotic Systems 2(4):363-370, December 2005.

[21] Dixon, C., Winfield , A.F.T., Fisher, M., and Zeng, C. Towards Temporal Verification of Swarm Robotic Systems. Robotics and Autonomous Systems, Elsevier, 2012

[22] Konur S., Dixon C., and Fisher M. Analysing Robot Swarm Behaviour via Probabilistic Model Checking Robotics and Autonomous Systems, 60(2):199-213 Elsevier, 2012

[23] W. Liu, A. Winfield, J. Sa, Modelling Swarm Robotic Systems: A Study in Collective Foraging, in: Proc. Towards Autonomous Robotic Systems (TAROS), pp. 25-32.

[24] W. Liu, A. Winfield, J. Sa, J. Chen, L. Dou, Strategies for Energy Optimisation in a Swarm of Foraging Robots, in: Proc. 2nd International Workshop on Swarm Robotics (SAB), volume 4433 of LNCS, Springer, 2007, pp. 14-26.

[25] A. Hinton, M. Kwiatkowska, G. Norman, D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, in: Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of LNCS, Springer, 2006, pp. 441-444.

[26] B. Konev, TRP++ Temporal Resolution Prover, http://www.csc.liv.ac.uk/%7Ekonev/software/trp++/

[27] M. Ludwig, TSPASS a fair monodic first-order temporal prover http://www.csc.liv.ac.uk/~michel/software/tspass/

[28] B. Konev, TeMP a Temporal Monodic Prover http://www.csc.liv.ac.uk/%7Ekonev/software/TeMP/

Reasoning in Exactly One Logics

(With Boris Konev)

Dynamic systems are those that change over time. Temporal logics are extensions of propositional logics that have operators to deal with time such as next (in the next moment in time) and eventuality (sometime in the future). These have been developed and and used to represent and reason about dynamic systems. The Logic and Computation Group are interested in developing techniques to apply and reason about such logics.

Resolution is a well known reasoning method for propositional and first order logics. In the Logic and Computation group at Liverpool we have extended this to temporal logics [30] and developed provers for propositional and first order temporal logics in [31,32,33].

When modelling realistic systems, there are often additional constraints that enforce that exactly one out of a set of conditions must hold. For example when representing the movement of a robot in a grid which is in some mode there are conditions stating that the robot must be in exactly one grid square and it must be in exactly one mode. The logic combining both temporal logic and constraints that limit of the number of propositions allowed to be true at any state from a set of propositions is known as TLC[35a]. A tableau-style reasoner for TLC has been developed in [35a]. This has the disadvantage of requiring formulae to be in a normal form and involves the explicit enumeration of the constraints.

In many cases exactly one constraints are required. The logic combining both temporal logic and exactly one constraints is known as TLX [34]. We have proposed an extension to the resolution calculus in [30] to such logics in [34].

This project involves further development, analysis, and application of exactly one constraints to temporal systems. Initially the calculus in [34] can be used as the basis to developing, implementing and applying a resolution prover for propositional temporal logics allowing exactly one constraints. Depending on the outcome of this, further developments may be improvements to the propositional exactly-one calculus or focussed on developing a first-order version of the calculus eg for reasoning in parameterised systems [35].

Another avenue to explore would be to investigate recent advances in hardware verification eg [35b,35c] and examine the similarities and differences with [30].

References

[30] Fisher, M., Dixon, C., and Peim, M. Clausal Temporal Resolution, ACM Transactions on Computational Logic, volume 2, number 1, January 2001

[31] B. Konev, TRP++ Temporal Resolution Prover, http://www.csc.liv.ac.uk/%7Ekonev/software/trp++/

[32] M. Ludwig, TSPASS a fair monodic first-order temporal prover http://www.csc.liv.ac.uk/~michel/software/tspass/

[33] B. Konev, TeMP a Temporal Monodic Prover http://www.csc.liv.ac.uk/%7Ekonev/software/TeMP/

[34] Dixon, C., Fisher, M., and Konev, B., Tractable Temporal Reasoning in the Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07), pages 318-323, January 6-12th 2007, Hyderabad, India

[35] Dixon, C., Fisher, M., Konev, B., and Lisitsa, A., Practical First-Order Temporal Reasoning in the Proceedings of TIME 2008, 16th-18th June 2008, Montreal, Canada. IEEE Press.

[35a] Dixon, C., Konev, B., Fisher, M., and Nietiadi, S. Deductive Temporal Reasoning with Constraints Journal of Applied Logic, 11(1): 30-51, Elsevier, 2013

[35b] Bradley A.R., SAT-Based Model Checking without Unrolling. VMCAI 2011: 70-87

[35c] Claessen, K., and Sorensson, N., A Liveness Checking Algorithm that Counts FMCAD12, 2012: 52-59

Temporal Planning

Planning[30] is an active research area in the field of Artificial Intelligence. Given a set of initial conditions, a set of actions and a goal the problem is to find a suitable sequence of actions that can take us from the initial conditions to the goal.

Planning problems can be described in the "Planning Domain Definition Language" (PDDL)[31]. A collection of benchmark problems, in PDDL, are provided for the bi-annual International Planning Competition (IPPC) [32]. A well known planning problem is that of 'Blocks World'. Given a number of blocks on a table which may or may not be stacked on top of each other initially, and a robot arm which can pick up a block, one at a time, from the top of a stack and place it on another block or on the table the goal is to find a sequence or actions (pickup, stack etc) to construct a tower where, the blocks are in a particular order. This apparently simple problem is still challenging for many planners.

Planning can be viewed as theorem proving by checking to see whether the description of the planning problem, SPEC, given in some logical language, is satisfiable. The model on which the SPEC holds can be used to construct a plan which satisfies the given problem. Temporal logic seems a suitable choice to formulate planning problems as, initial conditions can be represented as formulae holding in the initial state, actions can be modelled by making a next step and recording that the action that has been taken, goals can be represented using eventualities and invariants can be modelled using the 'always' operator. Given a planning problem represented in temporal logic we can use tools such as propositional and first-order theorem provers TRP++, TeMP and TSPASS [33,34,35] apply this approach experimentally.

Other authors have considered applying temporal logics to planning, see for example[36,37].

Recent work relating to temporal logics which allow sets of propositions where "exactly one" from this set must hold at any moment[38,39,40] may be applicable in this domain. Such "exactly one" sets seem to occur in planning (for example if exactly one action is allowed to be performed at any moment) and make reasoning about such problems simpler.

The aim of this project is apply temporal logics and related tools to the planning problem. Initially a translation from PDDL descriptions to temporal logic syntax, suitable for input to our proof tools, will be developed and implemented. An analysis of the usefulness of "exactly one" sets will also be carried out. This will then be useful in assessing how much of PDDL can be translated into temporal logic as well as how well our proof tools handle such planning problems. The latter will provide us with experimental data showing which types of planning problems our provers do well or badly at, in comparison with standard planners. In the longer term this will lead to us focusing on a particular sub-field of planning particularly suited to this approach or developing temporal logic techniques which may help standard planners find solutions. Dependent on the preliminary findings, this project may involve the development of theorem provers to allow proofs in the chosen planning sub-field or the inclusion of temporal aspects to existing provers.

References

[30] M.Ghallab, D.Nau and P.Traverso Automated Planning: Theory & Practice: (The Morgan Kaufmann Series in Artificial Intelligence) Morgan Kaufmann, 2004

[31] M. Fox and D. Long (2003) PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains, Journal of Artificial Intelligence Research, Volume 20, pages 61-124

[32] IPPC 2008 Results. http://ippc-2008.loria.fr/wiki/index.php/Results

[33] B. Konev, TRP++ Temporal Resolution Prover, http://www.csc.liv.ac.uk/%7Ekonev/software/trp++/

[34] B. Konev, TeMP a Temporal Monodic Prover http://www.csc.liv.ac.uk/%7Ekonev/software/TeMP/

[35] M. Ludwig, TSPASS a fair monodic first-order temporal prover http://www.csc.liv.ac.uk/~michel/software/tspass/

[36] S.Cerrito and M. Cialdea Mayer Using linear temporal logic to model and solve planning problems Lecture Notes in Computer Science, Volume 1480, Springer.1998

[37] K.T.Seown and M.Pasquier, Vehicle route-sequence planning using temporal logic, Artificial Intelligence Engineering Design, Analysis and Manufacturing, 16(1):31--38, 2002. Cambridge University Press

[38] C. Dixon, M. Fisher and B. Konev, Tractable Temporal Reasoning, in the Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07), pages 318-323, January 6-12th 2007, Hyderabad, India

[39] C.Dixon, M.Fisher and B.Konev, Temporal Logic with Capacity Constraints, in the Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS), September 10-12, Liverpool, UK. LNAI, Springer 2007.

[40] C.Dixon, M. Fisher, B.Konev and A.Lisitsa, Practical First-Order Temporal Reasoning, in the Proceedings of TIME 2008, 16th-18th June 2008, Montreal, Canada. IEEE Press.