Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths

Davide Bresolin; Valentin Goranko; Angelo Montanari; Guido Sciavicco

doi:10.1109/SEFM.2009.36

Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths

Davide Bresolin, Valentin Goranko, Angelo Montanari, Guido Sciavicco

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

Original language	English
Title of host publication	Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009)
Publisher	IEEE Computer Society Press
Publication date	2009
Pages	240-249
ISBN (Print)	978-0-7695-3870-9
DOIs	https://doi.org/10.1109/SEFM.2009.36
Publication status	Published - 2009
Event	Seventh IEEE International Conference on Software Engineering and Formal Methods - Hanoi, Viet Nam Duration: 23 Nov 2009 → 27 Nov 2009 Conference number: 7 https://ieeexplore.ieee.org/xpl/conhome/5368044/proceeding

Conference

Conference	Seventh IEEE International Conference on Software Engineering and Formal Methods
Number	7
Country/Territory	Viet Nam
City	Hanoi
Period	23/11/2009 → 27/11/2009
Internet address	https://ieeexplore.ieee.org/xpl/conhome/5368044/proceeding

Access to Document

10.1109/SEFM.2009.36

OpenUrl availability

Full text

Cite this

@inproceedings{916506ec1aed4ca09bf072feb4cc22da,

title = "Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths",

abstract = "Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.",

author = "Davide Bresolin and Valentin Goranko and Angelo Montanari and Guido Sciavicco",

year = "2009",

doi = "10.1109/SEFM.2009.36",

language = "English",

isbn = "978-0-7695-3870-9",

pages = "240--249",

booktitle = "Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009)",

publisher = "IEEE Computer Society Press",

note = "Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009 ; Conference date: 23-11-2009 Through 27-11-2009",

url = "https://ieeexplore.ieee.org/xpl/conhome/5368044/proceeding",

}

Bresolin, D, Goranko, V, Montanari, A & Sciavicco, G 2009, Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths. in Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009). IEEE Computer Society Press, pp. 240-249, Seventh IEEE International Conference on Software Engineering and Formal Methods, Hanoi, Viet Nam, 23/11/2009. https://doi.org/10.1109/SEFM.2009.36

Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths. / Bresolin, Davide; Goranko, Valentin; Montanari, Angelo et al.
Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009). IEEE Computer Society Press, 2009. p. 240-249.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths

AU - Bresolin, Davide

AU - Goranko, Valentin

AU - Montanari, Angelo

AU - Sciavicco, Guido

N1 - Conference code: 7

PY - 2009

Y1 - 2009

N2 - Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

AB - Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

U2 - 10.1109/SEFM.2009.36

DO - 10.1109/SEFM.2009.36

M3 - Article in proceedings

SN - 978-0-7695-3870-9

SP - 240

EP - 249

BT - Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009)

PB - IEEE Computer Society Press

T2 - Seventh IEEE International Conference on Software Engineering and Formal Methods

Y2 - 23 November 2009 through 27 November 2009

ER -

Right Propositional Neighborhood Logic over Natural Numbers with Integer Constraints for Interval Lengths

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this