Model Checking One-clock Priced Timed Automata

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities....

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2008-06, Vol.4, Issue 2 (2:9)
Main Authors: Bouyer, Patricia, Larsen, Kim G., Markey, Nicolas
Format: Article
Language:English
Subjects:
Computer Science
computer science - computational complexity
computer science - computer science and game theory
computer science - logic in computer science
f.1.1
f.3.1
Logic in Computer Science
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c382t-1b2fb10b20edfa4dd06619ec36276bc66ff2f832302ed8f83d05db56cfeebcb73
cites
container_end_page
container_issue 2:9
container_start_page
container_title Logical methods in computer science
container_volume 4, Issue 2
creator Bouyer, Patricia
Larsen, Kim G.
Markey, Nicolas
description We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).
doi_str_mv 10.2168/LMCS-4(2:9)2008
format article
fullrecord <record><control><sourceid>hal_doaj_</sourceid><recordid>TN_cdi_doaj_primary_oai_doaj_org_article_23c258543158475284c002a06d22a38b</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><doaj_id>oai_doaj_org_article_23c258543158475284c002a06d22a38b</doaj_id><sourcerecordid>oai_HAL_hal_01194599v1</sourcerecordid><originalsourceid>FETCH-LOGICAL-c382t-1b2fb10b20edfa4dd06619ec36276bc66ff2f832302ed8f83d05db56cfeebcb73</originalsourceid><addsrcrecordid>eNpVkM1Lw0AQxRdRsNSeveZoD2l3Zz-y8VaC2kJKBet52c82bdpIEgX_exMjonOYeTze_A4PoVuCZ0CEnOfr7CVmd3CfTgFjeYFGRAoc8zRhl3_0NZo0zQF3QymRIEZotq6cL6Ns7-2xOO-izdnHtqzsMXquC-tdtC1O3V68t9VJt_oGXQVdNn7yc8fo9fFhmy3jfPO0yhZ5bKmENiYGgiHYAPYuaOYcFoKk3lIBiTBWiBAgSAoUg3eyUw5zZ7iwwXtjTULHaDVwXaUP6q0uTrr-VJUu1LdR1Tul67awpVdALXDJGSVcsoSDZBZj0Fg4AE2l6VjTgbXX5T_UcpGr3sOEpIyn6QfpsvMha-uqaWoffh8IVn3Tqm9aMQUqVX3T9AveS23_</addsrcrecordid><sourcetype>Open Website</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>Model Checking One-clock Priced Timed Automata</title><source>EZB Electronic Journals Library</source><creator>Bouyer, Patricia ; Larsen, Kim G. ; Markey, Nicolas</creator><creatorcontrib>Bouyer, Patricia ; Larsen, Kim G. ; Markey, Nicolas</creatorcontrib><description>We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).</description><identifier>ISSN: 1860-5974</identifier><identifier>EISSN: 1860-5974</identifier><identifier>DOI: 10.2168/LMCS-4(2:9)2008</identifier><language>eng</language><publisher>Logical Methods in Computer Science Association</publisher><subject>Computer Science ; computer science - computational complexity ; computer science - computer science and game theory ; computer science - logic in computer science ; f.1.1 ; f.3.1 ; Logic in Computer Science</subject><ispartof>Logical methods in computer science, 2008-06, Vol.4, Issue 2 (2:9)</ispartof><rights>Distributed under a Creative Commons Attribution 4.0 International License</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c382t-1b2fb10b20edfa4dd06619ec36276bc66ff2f832302ed8f83d05db56cfeebcb73</citedby><orcidid>0000-0003-1977-7525 ; 0000-0002-2823-0911</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>230,314,776,780,881,27901,27902</link.rule.ids><backlink>$$Uhttps://hal.science/hal-01194599$$DView record in HAL$$Hfree_for_read</backlink></links><search><creatorcontrib>Bouyer, Patricia</creatorcontrib><creatorcontrib>Larsen, Kim G.</creatorcontrib><creatorcontrib>Markey, Nicolas</creatorcontrib><title>Model Checking One-clock Priced Timed Automata</title><title>Logical methods in computer science</title><description>We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).</description><subject>Computer Science</subject><subject>computer science - computational complexity</subject><subject>computer science - computer science and game theory</subject><subject>computer science - logic in computer science</subject><subject>f.1.1</subject><subject>f.3.1</subject><subject>Logic in Computer Science</subject><issn>1860-5974</issn><issn>1860-5974</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2008</creationdate><recordtype>article</recordtype><sourceid>DOA</sourceid><recordid>eNpVkM1Lw0AQxRdRsNSeveZoD2l3Zz-y8VaC2kJKBet52c82bdpIEgX_exMjonOYeTze_A4PoVuCZ0CEnOfr7CVmd3CfTgFjeYFGRAoc8zRhl3_0NZo0zQF3QymRIEZotq6cL6Ns7-2xOO-izdnHtqzsMXquC-tdtC1O3V68t9VJt_oGXQVdNn7yc8fo9fFhmy3jfPO0yhZ5bKmENiYGgiHYAPYuaOYcFoKk3lIBiTBWiBAgSAoUg3eyUw5zZ7iwwXtjTULHaDVwXaUP6q0uTrr-VJUu1LdR1Tul67awpVdALXDJGSVcsoSDZBZj0Fg4AE2l6VjTgbXX5T_UcpGr3sOEpIyn6QfpsvMha-uqaWoffh8IVn3Tqm9aMQUqVX3T9AveS23_</recordid><startdate>20080620</startdate><enddate>20080620</enddate><creator>Bouyer, Patricia</creator><creator>Larsen, Kim G.</creator><creator>Markey, Nicolas</creator><general>Logical Methods in Computer Science Association</general><general>Logical Methods in Computer Science e.V</general><scope>AAYXX</scope><scope>CITATION</scope><scope>1XC</scope><scope>VOOES</scope><scope>DOA</scope><orcidid>https://orcid.org/0000-0003-1977-7525</orcidid><orcidid>https://orcid.org/0000-0002-2823-0911</orcidid></search><sort><creationdate>20080620</creationdate><title>Model Checking One-clock Priced Timed Automata</title><author>Bouyer, Patricia ; Larsen, Kim G. ; Markey, Nicolas</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c382t-1b2fb10b20edfa4dd06619ec36276bc66ff2f832302ed8f83d05db56cfeebcb73</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2008</creationdate><topic>Computer Science</topic><topic>computer science - computational complexity</topic><topic>computer science - computer science and game theory</topic><topic>computer science - logic in computer science</topic><topic>f.1.1</topic><topic>f.3.1</topic><topic>Logic in Computer Science</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Bouyer, Patricia</creatorcontrib><creatorcontrib>Larsen, Kim G.</creatorcontrib><creatorcontrib>Markey, Nicolas</creatorcontrib><collection>CrossRef</collection><collection>Hyper Article en Ligne (HAL)</collection><collection>Hyper Article en Ligne (HAL) (Open Access)</collection><collection>DOAJ Directory of Open Access Journals</collection><jtitle>Logical methods in computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Bouyer, Patricia</au><au>Larsen, Kim G.</au><au>Markey, Nicolas</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Model Checking One-clock Priced Timed Automata</atitle><jtitle>Logical methods in computer science</jtitle><date>2008-06-20</date><risdate>2008</risdate><volume>4, Issue 2</volume><issue>2:9</issue><issn>1860-5974</issn><eissn>1860-5974</eissn><abstract>We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities. We prove that, under the assumption that the model has only one clock, model-checking this class of models against the logic WCTL, CTL with cost-constrained modalities, is PSPACE-complete (while it has been shown undecidable as soon as the model has three clocks). We also prove that model-checking WMTL, LTL with cost-constrained modalities, is decidable only if there is a single clock in the model and a single stopwatch cost variable (i.e., whose slopes lie in {0,1}).</abstract><pub>Logical Methods in Computer Science Association</pub><doi>10.2168/LMCS-4(2:9)2008</doi><orcidid>https://orcid.org/0000-0003-1977-7525</orcidid><orcidid>https://orcid.org/0000-0002-2823-0911</orcidid><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 1860-5974
ispartof Logical methods in computer science, 2008-06, Vol.4, Issue 2 (2:9)
issn 1860-5974
1860-5974
language eng
recordid cdi_doaj_primary_oai_doaj_org_article_23c258543158475284c002a06d22a38b
source EZB Electronic Journals Library
subjects Computer Science
computer science - computational complexity
computer science - computer science and game theory
computer science - logic in computer science
f.1.1
f.3.1
Logic in Computer Science
title Model Checking One-clock Priced Timed Automata
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-02-10T16%3A04%3A16IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-hal_doaj_&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Model%20Checking%20One-clock%20Priced%20Timed%20Automata&rft.jtitle=Logical%20methods%20in%20computer%20science&rft.au=Bouyer,%20Patricia&rft.date=2008-06-20&rft.volume=4,%20Issue%202&rft.issue=2:9&rft.issn=1860-5974&rft.eissn=1860-5974&rft_id=info:doi/10.2168/LMCS-4(2:9)2008&rft_dat=%3Chal_doaj_%3Eoai_HAL_hal_01194599v1%3C/hal_doaj_%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c382t-1b2fb10b20edfa4dd06619ec36276bc66ff2f832302ed8f83d05db56cfeebcb73%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true