Abstrakt. I det här dokumentet studerar vi modellkontroll- och parametersyntesproblemen hos logiken TCTL över diskret timad automata där parametrar är tillåtna både i modellen (timed automaton) och i egenskapen (temporal formel). Våra resultat är som följer. På den negativa sidan visar vi att problemet med modellkontroll av TCTL-utökad med parametrar är oavgjort över diskret timad automata med endast en parametrisk klocka. Obeslutbarhetsresultatet kräver jämlikhet i logiken. På den positiva sidan visar vi att modellkontroll- och parametersyntesproblemen blir avgörande för ett fragment av logiken där jämlikhet inte är tillåtet. Vår metod är baserad på automatiska teoretiska principer och en förlängning av vår metod för att uttrycka durationer av körningar i tidsinställd automata med hjälp av Presburger aritmetik.
Parametersyntesproblem för förgreningstidslogiken TCTL studeras i REF, där parametrar anges både i modellen och formeln.
Real-time model-checking: Parameters everywhere
{'venue': 'In 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’03', 'journal': None, 'mag_field_of_study': ['Computer Science']}