Model Checking ?-Calculus in Well-Structured Transition Systems

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by E. V. Kouzmin Articles by N. V. Shilov Articles by V. A. Sokolov

11th International Symposium on Temporal Representation and Reasoning (TIME'04)

Tatihou, Normandie, France

July 01-July 03

ISBN: 0-7695-2155-X

	ASCII Text	x
	E. V. Kouzmin, N. V. Shilov, V. A. Sokolov, "Model Checking ?-Calculus in Well-Structured Transition Systems," Temporal Representation and Reasoning, International Syposium on, pp. 152-155, 11th International Symposium on Temporal Representation and Reasoning (TIME'04), 2004.

	BibTex	x
	@article{ 10.1109/TIME.2004.1314433, author = {E. V. Kouzmin and N. V. Shilov and V. A. Sokolov}, title = {Model Checking ?-Calculus in Well-Structured Transition Systems}, journal ={Temporal Representation and Reasoning, International Syposium on}, volume = {0}, year = {2004}, issn = {1530-1311}, pages = {152-155}, doi = {http://doi.ieeecomputersociety.org/10.1109/TIME.2004.1314433}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Temporal Representation and Reasoning, International Syposium on TI - Model Checking ?-Calculus in Well-Structured Transition Systems SN - 1530-1311 SP152 EP155 A1 - E. V. Kouzmin, A1 - N. V. Shilov, A1 - V. A. Sokolov, PY - 2004 KW - null VL - 0 JA - Temporal Representation and Reasoning, International Syposium on ER -

E. V. Kouzmin, Yaroslavl State University

N. V. Shilov, Institute of Informatics Systems

V. A. Sokolov, Yaroslavl State University

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2004.1314433

We study the model checking problem for fixpoint logics in well-structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality) properties in well-structured single action transition systems. Our main result is as follows: the model checking problem is decidable for disjunctive formulae of the propositional ?-Calculus of D. Kozen (1983) in well-structured transition systems where propositional variables are interpreted by upward cones. We also discuss the model checking problem for the intuitionistic modal logic of Fisher Servi (1984) extended by least fixpoint.

Citation:

E. V. Kouzmin, N. V. Shilov, V. A. Sokolov, "Model Checking ?-Calculus in Well-Structured Transition Systems," time, pp.152-155, 11th International Symposium on Temporal Representation and Reasoning (TIME'04), 2004

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.