Thumbnail
Access Restriction
Subscribed

Author Courcoubetis, Costas ♦ Yannakakis, Mihalis
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1995
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword EXPTIME-complete ♦ Markov chain ♦ PSPACE-complete ♦ Automata ♦ Model checking ♦ Probabilistic algorithm ♦ Temporal logic
Abstract We determine the complexity of testing whether a finite state, sequential or concurrent probabilistic program satisfies its specification expressed in linear-time temporal logic. For sequential programs, we present an algorithm that runs in time linear in the program and exponential in the specification, and also show that the problem is in PSPACE, matching the known lower bound. For concurrent programs, we show that the problem can be solved in time polynomial in the program and doubly exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifications described by ω-automata or formulas in extended temporal logic.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1995-07-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 42
Issue Number 4
Page Count 51
Starting Page 857
Ending Page 907


Open content in new tab

   Open content in new tab
Source: ACM Digital Library