A Decision Method for Duration Calculus
Дата
Авторы
Chetcuti-Sperandio,Nathalie
Cerro,Luis Fariñas del
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
The Duration Calculus is an interval logic introduced for designing real-time systems. This calculus is able to capture important real-time problems like the specification of the behaviours of schedulers and classical examples like a gas burner. From a practical point of view an important challenge becomes to define automated proof procedures for this calculus. Since the propositional calculus is undecidable, we are interested then into isolating decidable fragments of this calculus. A first fragment was given and its decidability proved via regular languages. In this paper we isolate another fragment and we define a tableau method which gives a natural procedure to decide whether a given formula is satisfiable. This fragment is strong enough to embed Allen's Interval Algebra.
Ключевые слова
Duration Calculus , automated deduction , tableau method