License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2019.16
URN: urn:nbn:de:0030-drops-113748
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11374/
Go to the corresponding LIPIcs Volume Portal

Zavatteri, Matteo ; Combi, Carlo ; Rizzi, Romeo ; Viganò, Luca

Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions

pdf-format:
LIPIcs-TIME-2019-16.pdf (0.6 MB)

Abstract

A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN by adding decision time points to model temporal plans with decisions. A decision time point is a special kind of time point that once executed allows for deciding a truth value for an associated Boolean proposition. Furthermore, STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i.e., complete truth value assignments to the propositions) they are relevant. Thus, an STND models a family of STNs each obtained as a projection of the initial STND onto a scenario. An STND is consistent if there exists a consistent scenario (i.e., a scenario such that the corresponding STN projection is consistent). Recently, a hybrid SAT-based consistency checking algorithm (HSCC) was proposed to check the consistency of an STND. Unfortunately, that approach lacks experimental evaluation and does not allow for the synthesis of all consistent scenarios. In this paper, we propose an incremental HSCC algorithm for STNDs that (i) is faster than the previous one and (ii) allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). Then, we carry out an experimental evaluation with KAPPA, a tool that we developed for STNDs. Finally, we prove that STNDs and disjunctive temporal networks (DTNs) are equivalent.

BibTeX - Entry

@InProceedings{zavatteri_et_al:LIPIcs:2019:11374,
  author =	{Matteo Zavatteri and Carlo Combi and Romeo Rizzi and Luca Vigan{\`o}},
  title =	{{Hybrid SAT-Based Consistency Checking Algorithms for Simple Temporal Networks with Decisions}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Johann Gamper and Sophie Pinchinat and Guido Sciavicco},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11374},
  URN =		{urn:nbn:de:0030-drops-113748},
  doi =		{10.4230/LIPIcs.TIME.2019.16},
  annote =	{Keywords: Simple temporal network with decisions, HSCC algorithms, incremental SAT-solving, disjunctive temporal network, KAPPA}
}

Keywords: Simple temporal network with decisions, HSCC algorithms, incremental SAT-solving, disjunctive temporal network, KAPPA
Collection: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Issue Date: 2019
Date of publication: 07.10.2019
Supplementary Material: https://github.com/matteozavatteri/kappa

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI