ridm@nrct.go.th   ระบบคลังข้อมูลงานวิจัยไทย   รายการโปรดที่คุณเลือกไว้

Verifying temporal properties of systems with applications to petri nets

หน่วยงาน Edinburgh Research Archive, United Kingdom

รายละเอียด

ชื่อเรื่อง : Verifying temporal properties of systems with applications to petri nets
นักวิจัย : Bradfield, Julian Charles
คำค้น : Computer programs , Verification , Petri nets
หน่วยงาน : Edinburgh Research Archive, United Kingdom
ผู้ร่วมงาน : Stirling, Colin
ปีพิมพ์ : 2534
อ้างอิง : http://hdl.handle.net/1842/6565
ที่มา : -
ความเชี่ยวชาญ : -
ความสัมพันธ์ : J. C. Bradfield, Proving temporal properties of Petri nets. Advances in Petrz Nets 1990 LNCS (1991). , J. C. Bradfield and C. P. Stirling, Verifying temporal properties of processes. Proc. CONCUR '90 115-125. LNCS 458 (1990). , J. C. Bradfield and C. P. Stirling, Local model checking for infinite state spaces. Theoret. Comput. Scz. (1991).
ขอบเขตของเนื้อหา : -
บทคัดย่อ/คำอธิบาย :

This thesis provides a powerful general-purpose proof technique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et al. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a relatively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relation on the state space defined by the tableau-the success of the tableau then depends on the well-foundedness of this relation. This development occupies the second and third chapters: the second considers the modal mu-calculus, and explains its power, while the third develops the tableau technique itself The generalized tableau technique is exhibited on Petri nets, and various standard notions from net theory are shown to play a part in the use of the technique on nets-in particular, the invariant calculus has a major role. The requirement for a finite presentation of tableaux for infinite systems raises the question of the expressive power of the mu-calculus. This is studied in some detail, and it is shown that on reasonably powerful models of computation, such as Petri nets, the mu-calculus can express properties that are not merely undecidable, but not even arithmetical. The concluding chapter discusses some of the many questions still to be answered, such as the incorporation of formal reasoning within the tableau system, and the power required of such reasoning.

บรรณานุกรม :
Bradfield, Julian Charles . (2534). Verifying temporal properties of systems with applications to petri nets.
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Bradfield, Julian Charles . 2534. "Verifying temporal properties of systems with applications to petri nets".
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom .
Bradfield, Julian Charles . "Verifying temporal properties of systems with applications to petri nets."
    กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2534. Print.
Bradfield, Julian Charles . Verifying temporal properties of systems with applications to petri nets. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2534.