On discretisable formulas in duration calculus

Authors:	Pham, Hong Thai
Keywords:	discretisable formulas;duration calculus
Issue Date:	2004
Publisher:	H. : ĐHQGHN
Series/Report no.:	Vol. 20;No. 1 (2004)
Abstract:	Model checking problem for real-time systems is a hard problem and has high complexity because time model of system is dense and continuous. Especially, as known, almost accumulated timed properties which are expressed by duration formulas in Duration Calculus is undecidable or decidable but with very high complexity. However, fortunately for some formulas, to avoid high complexity we can only check them in integral model of time instead of real time model. Such formulas are called discretisable formulas. In this paper, we show a subclass of formulas in Duration Calculus which is constructed from a linear constraint of state durations is discretisable and based on this we also give some ideas for checking them. The our results includes some results of the others.
Description:	p. 53-66
URI:	http://repository.vnu.edu.vn/handle/VNU_123/57893
ISSN:	2588-1124
Appears in Collections:	Mathematics and Physics