The language preservation problem is undecidable for parametric event-recording automata

Parametric timed automata (PTA) extend timed automata with unknown constants ("parameters"), at the price of undecidability of most interesting problems. The (untimed) language preservation problem ("given a parameter valuation, can we find at least one other valuation with the same u...

Full description

Saved in:
Bibliographic Details
Main Authors: André, Étienne, Lin, Shang-Wei
Other Authors: School of Computer Science and Engineering
Format: Article
Language:English
Published: 2020
Subjects:
Online Access:https://hdl.handle.net/10356/142707
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Nanyang Technological University
Language: English
Description
Summary:Parametric timed automata (PTA) extend timed automata with unknown constants ("parameters"), at the price of undecidability of most interesting problems. The (untimed) language preservation problem ("given a parameter valuation, can we find at least one other valuation with the same untimed language?") is undecidable for PTAs. We prove that this problem remains undecidable for parametric event-recording automata (PERAs), a subclass of PTAs that considerably restrains the way the language can be used; we also show it remains undecidable even for slightly different definitions of the language, i.e., finite sequences of actions ending in or passing infinitely often through accepting locations, or just all finite untimed words (without accepting locations).