<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.0 20120330//EN" "JATS-journalpublishing1.dtd"><article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" article-type="research-article"><front><journal-meta><journal-id journal-id-type="publisher-id">INFORMATICA</journal-id><journal-title-group><journal-title>Informatica</journal-title></journal-title-group><issn pub-type="epub">0868-4952</issn><issn pub-type="ppub">0868-4952</issn><publisher><publisher-name>VU</publisher-name></publisher></journal-meta><article-meta><article-id pub-id-type="publisher-id">inf23306</article-id><article-id pub-id-type="doi">10.15388/Informatica.2012.368</article-id><article-categories><subj-group subj-group-type="heading"><subject>Research article</subject></subj-group></article-categories><title-group><article-title>Applications of Finite Linear Temporal Logic to Piecewise Linear Aggregates</article-title></title-group><contrib-group><contrib contrib-type="Author"><name><surname>Pranevicius</surname><given-names>Henrikas</given-names></name><email xlink:href="mailto:henrikas.pranevicius@ktu.lt">henrikas.pranevicius@ktu.lt</email><xref ref-type="aff" rid="j_INFORMATICA_aff_000"/></contrib><contrib contrib-type="Author"><name><surname>Norgėla</surname><given-names>Stanislovas</given-names></name><email xlink:href="mailto:stasys.norgela@mif.vu.lt">stasys.norgela@mif.vu.lt</email><xref ref-type="aff" rid="j_INFORMATICA_aff_001"/></contrib><aff id="j_INFORMATICA_aff_000">The Faculty of Informatics, Kaunas University of Technology, Studentų 50, LT-51368 Kaunas, Lithuania</aff><aff id="j_INFORMATICA_aff_001">The Faculty of Mathematics and Informatics, Vilnius University, Naugarduko 24, LT-03225 Vilnius, Lithuania</aff></contrib-group><pub-date pub-type="epub"><day>01</day><month>01</month><year>2012</year></pub-date><volume>23</volume><issue>3</issue><fpage>427</fpage><lpage>441</lpage><history><date date-type="received"><day>01</day><month>07</month><year>2010</year></date><date date-type="accepted"><day>01</day><month>06</month><year>2012</year></date></history><abstract><p>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.</p></abstract><kwd-group><label>Keywords</label><kwd>artificial knowledge representation</kwd><kwd>artificial intelligence planning</kwd><kwd>piecewise linear aggregates</kwd><kwd>finite linear temporal logic</kwd></kwd-group></article-meta></front></article>