Costs and rewards in priced timed automata

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend o...

Full description

Bibliographic Details
Main Authors: Fränzle, M, Shirmohammadi, M, Swaminathan, M, Worrell, J
Format: Journal article
Language:English
Published: Schloss Dagstuhl 2018
_version_ 1797101138236932096
author Fränzle, M
Shirmohammadi, M
Swaminathan, M
Worrell, J
author_facet Fränzle, M
Shirmohammadi, M
Swaminathan, M
Worrell, J
author_sort Fränzle, M
collection OXFORD
description We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an ε-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10thProblem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
first_indexed 2024-03-07T05:47:37Z
format Journal article
id oxford-uuid:e7bed8b9-ed4c-44a7-952b-f8184b0c4360
institution University of Oxford
language English
last_indexed 2024-03-07T05:47:37Z
publishDate 2018
publisher Schloss Dagstuhl
record_format dspace
spelling oxford-uuid:e7bed8b9-ed4c-44a7-952b-f8184b0c43602022-03-27T10:41:15ZCosts and rewards in priced timed automataJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:e7bed8b9-ed4c-44a7-952b-f8184b0c4360EnglishSymplectic Elements at OxfordSchloss Dagstuhl2018Fränzle, MShirmohammadi, MSwaminathan, MWorrell, JWe consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an ε-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10thProblem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.
spellingShingle Fränzle, M
Shirmohammadi, M
Swaminathan, M
Worrell, J
Costs and rewards in priced timed automata
title Costs and rewards in priced timed automata
title_full Costs and rewards in priced timed automata
title_fullStr Costs and rewards in priced timed automata
title_full_unstemmed Costs and rewards in priced timed automata
title_short Costs and rewards in priced timed automata
title_sort costs and rewards in priced timed automata
work_keys_str_mv AT franzlem costsandrewardsinpricedtimedautomata
AT shirmohammadim costsandrewardsinpricedtimedautomata
AT swaminathanm costsandrewardsinpricedtimedautomata
AT worrellj costsandrewardsinpricedtimedautomata