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

Research output: Research - peer-reviewArticle in proceedings – Annual report year: 2009

View graph of relations

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 languageEnglish
Title of host publicationProceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'2009)
PublisherIEEE Computer Society Press
Publication date2009
Pages240-249
ISBN (Print)978-0-7695-3870-9
DOIs
StatePublished - 2009
Event7th IEEE International Conference on Software Engineering and Formal Methods - Hanoi, Vietnam
Duration: 1 Jan 2009 → …

Conference

Conference7th IEEE International Conference on Software Engineering and Formal Methods
CityHanoi, Vietnam
Period01/01/2009 → …
CitationsWeb of Science® Times Cited: 10
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

ID: 5541632