Applications of Finite Linear Temporal Logic to Piecewise Linear Aggregates

Article type: Research Article

Authors: Pranevicius, Henrikas | Norgėla, Stanislovas

Affiliations: The Faculty of Informatics, Kaunas University of Technology, Studentų 50, LT-51368 Kaunas, Lithuania. E-mail: henrikas.pranevicius@ktu.lt | The Faculty of Mathematics and Informatics, Vilnius University, Naugarduko 24, LT-03225 Vilnius, Lithuania. E-mail: stasys.norgela@mif.vu.lt

Abstract: In this paper, we consider piecewise linear aggregates (PLA) and a possibility to use a linear temporal logic for analysis of their performance over finite structures (finite linear temporal logic (LTL)). We describe a calculus where the search is performed with respect to a context of the formula. An important aspect of finite LTL is the simplicity of its model of time and actions. PLA is used for description of numerous complex systems. The answers about the behavior of the aggregate are got by finding an interpretation in which all the formulas describing the work of the aggregate are true. This is illustrated by formalizing alternative bit protocol (ABP) task. We describe the ABP by putting it in the form of a planning problem. From the obtained model, we can find a finite sequence of actions to be executed in order to achieve the goal. In addition, an alternative bit protocol problem is described using the planning domain description language (PDDL). We report the results of experiments conducted using the LPG-TD planner.

Keywords: artificial knowledge representation, artificial intelligence planning, piecewise linear aggregates, finite linear temporal logic

Journal: Informatica, vol. 23, no. 3, pp. 427-441, 2012