
doi: 10.1109/time.2015.25
handle: 11390/1070685 , 11392/2332602
The chop operator C is a binary modality that plays an important role in interval temporal logics. Such an operator, which is not definable in Halpern and Shoham's modal logic of time intervals HS, allows one to split an interval into two parts and to specify what is true over them. C appears both in Moszkowski's PITL (that pairs it with a modal constant Pi which is true on all and only the intervals with coincident endpoints) and in Venema's CDT (that also features the binary modalities D and T, and Pi). Without the so-called locality principle, which restricts the semantics of proposition letters, the satisfiability problem for both PITL and CDT turns out to be undecidable over all meaningful classes of linear orders. The problem has been shown to be undecidable also for the fragment C, that is, PITL without Pi, over infinite linear orders. In this paper, we prove that the same holds for C over finite linear orders. To this end, we exploit the close relation between C and the reflexive version of the HS fragment BE, whose modalities correspond to Allen's relations starts and finishes: we prove that the satisfiability problem for reflexive BE is undecidable, undecidability of the same problem for C comes as a corollary.
Decidability, Interval Temporal Logics, Satisfiability Checking, Interval Temporal Logics; Satisfiability Checking; Decidability
Decidability, Interval Temporal Logics, Satisfiability Checking, Interval Temporal Logics; Satisfiability Checking; Decidability
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
