{"entities":{"Q1127817":{"pageid":1138566,"ns":120,"title":"Item:Q1127817","lastrevid":66190575,"modified":"2026-04-12T08:09:45Z","type":"item","id":"Q1127817","labels":{"en":{"language":"en","value":"Polytime model checking for times probabilistic computation tree logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1186249"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1127817$CF08B109-B7BE-437A-9377-7A398DF92597","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7aaaf1037077e73b79fa5aeb282a84944b643e46","datavalue":{"value":{"text":"Polytime model checking for times probabilistic computation tree logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1127817$FDFB13AF-DDA0-47CC-8BAF-C17F20CDADA4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b977b167d302b9e02409d387996e32f5b5876080","datavalue":{"value":"0910.68201","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$20EBA90D-A596-4590-AF2B-AD4EC02DAFE6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6eb8212826bd69dc98444cbd64b58f086206d659","datavalue":{"value":{"entity-type":"item","numeric-id":234698,"id":"Q234698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1127817$2E98A4C3-0246-455F-959D-294086EEFEA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d150572e8b9bb6a5fa32f12fda85c9aad1b71ca","datavalue":{"value":{"entity-type":"item","numeric-id":234699,"id":"Q234699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1127817$963E0D46-5F63-4FAA-83B3-52E2D48EA071","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1127817$83710908-31DE-4830-BB65-A7BBA7359195","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6a4a23ba804c9ca0ccf26f0d1fc2c3d7c165a953","datavalue":{"value":{"time":"+1999-03-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1127817$6341D1F5-22AA-4EA3-9EE3-C898F96226C1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"68765a9b244a09b56c3d42e4508561095c9ca1ce","datavalue":{"value":"We consider the model checking problem for timed probabilistic computation tree logic (TPCTL) introduced by H. A. Hansson and D. Jonsson, and studied in a recent book by \\textit{H. A. Hansson} ``Time and probability in formal design of distributed systems'' (Elsevier, 1994). The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in this book that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, some polytime decidable classes are described in the cited book, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1127817$C9490C22-5239-40DB-A651-108C485F7A87","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62ae2f4e9717dc72a20d2c4f17bdde30d85a417c","datavalue":{"value":"68T27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$81317622-2B89-4EDC-AF54-F4E537B0D48E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$C50D8086-4D7F-4B1C-8FD1-4894CB69ED21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1de3565cfd3393000dd87ca545f95ff84d4c1446","datavalue":{"value":"68W10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$4C5C3B90-6B08-465F-898A-7EBA92A4F9B0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0f61db66199013cabe6da24c4ecefb754f2df538","datavalue":{"value":"1186249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$11685FF4-FE26-4335-81CC-FC9AA14CD758","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85c0495ecb2ebf2281b5bf87af638a0062179162","datavalue":{"value":"polytime algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1127817$C730FC6A-E119-49F4-B452-7D6E474B1BC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"81e2968484318d9c5a7045c9cc7f3ff7582ddead","datavalue":{"value":"timed probabilistic computation tree logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1127817$B609C102-70D2-4787-9EF9-A1E14113038C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40971f5033e11f76c9ec957ec1402dd595b290ad","datavalue":{"value":"probabilistic transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1127817$CF9352EA-33C4-4ECF-ACEB-AD64F594DFE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1127817$A008D756-2B9E-4D6A-9A94-25F12185D2D7","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1127817$CFD747C5-52BC-45F6-9B0C-422006CBC6E5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f09beba92ab2d7744d805c15935df3673f108b40","datavalue":{"value":"https://doi.org/10.1007/s002360050136","type":"string"},"datatype":"url"},"type":"statement","id":"Q1127817$9B5E0180-0954-4504-AB00-3184ACC5A589","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ff9792afa832f04bfd3dc94d28d4348e3e2d89f0","datavalue":{"value":"W1999733611","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$C1B782F2-BE26-4DFF-A255-6BB6AE045D0E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a0696c2b3a69a378f803d6e29887e6a919cdfa2f","datavalue":{"value":"10.1007/S002360050136","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1127817$C609339A-0C29-40F2-8BE4-E20F6E5CAECA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab49dd9b477f3e4628229a95f94a5c17244fc7d4","datavalue":{"value":{"entity-type":"item","numeric-id":3400533,"id":"Q3400533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"576f226ce43de55072256ed07efe6f0bd7047ec8","datavalue":{"value":{"amount":"+0.8051013946533203","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1127817$70915123-4518-443F-B1FD-C1AC3CA6F15E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"684ae8713c9dd9a87dfbc129bc87879be0efd8b6","datavalue":{"value":{"entity-type":"item","numeric-id":1853732,"id":"Q1853732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45873c439b12a560e0351318766b1e5277dd964f","datavalue":{"value":{"amount":"+0.8042486906051636","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1127817$F6CA301D-65A9-4D77-A31A-A44C968CBB6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"320b564d9f4f19744106617d05644e9d8840469a","datavalue":{"value":{"entity-type":"item","numeric-id":2956706,"id":"Q2956706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74f8a5f1adcceb921b86dd00f3f5e509e2d285e9","datavalue":{"value":{"amount":"+0.8017014861106873","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1127817$DC2783E2-0973-452F-A3DE-482F8C9FCB11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"317b41ac22d4de40b461162d87f188bc7bd0c31d","datavalue":{"value":{"entity-type":"item","numeric-id":5758106,"id":"Q5758106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98cfc8fd60b894fa7f9e2ad01f1b3f44287246f3","datavalue":{"value":{"amount":"+0.7997771501541138","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1127817$11DF7C79-9CD6-468A-9112-C416EF076104","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f93fca35aff7bd285b30f3bbca171f54402ecc5","datavalue":{"value":{"entity-type":"item","numeric-id":3535619,"id":"Q3535619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"76c068f2ca4fe921a8eb8a0f268b4d97818cd17e","datavalue":{"value":{"amount":"+0.7969170212745667","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1127817$CBC7D94E-6763-4228-A1ED-875535AE8626","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Polytime model checking for times probabilistic computation tree logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Polytime_model_checking_for_times_probabilistic_computation_tree_logic"}}}}}