کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662930 | 1345211 | 2014 | 22 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Temporal logics for concurrent recursive programs: Satisfiability and model checking
ترجمه فارسی عنوان
منطق زمانی برای برنامه های بازگشت مجدد همزمان: رضایت و بررسی مدل
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
منطق زمانی؛ برنامه های بازگشتی همزمان؛ کلمات تو در تو. اثرات Mazurkiewicz؛ رضایت؛ چک کردن مدل
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic second-order logic and which, in addition, allows PDL-like path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 12, Issue 4, December 2014, Pages 395–416
Journal: Journal of Applied Logic - Volume 12, Issue 4, December 2014, Pages 395–416
نویسندگان
Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, Marc Zeitoun,