A Myhill-Nerode characterization for one-clock deterministic timed automata enables L*-style active learning of the canonical automaton.
A Theory of Timed Automata
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
verdicts
UNVERDICTED 5representative citing papers
A Maude-with-SMT framework for sound and complete formal analysis and parameter synthesis of parametric time Petri nets, including a folding approach that terminates on finite parametric state-class graphs and support for LTL model checking.
Presents parametric extrapolation for dense integer-complete underapproximation of parameter sets in bounded PTAs, with terminating algorithms for reachability and related properties.
An algorithm computes the bandwidth of normal timed automata by reducing the problem to finding the maximum reward-to-cost ratio in a weighted finite graph built from the automaton.
AL*RTA learns alternating real-time automata, terminates, and produces smaller models than NL*RTA at the expense of more queries while preserving expressive power.
citing papers explorer
-
A Myhill-Nerode Characterization and Active Learning for One-Clock Timed Automata
A Myhill-Nerode characterization for one-clock deterministic timed automata enables L*-style active learning of the canonical automaton.
-
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
A Maude-with-SMT framework for sound and complete formal analysis and parameter synthesis of parametric time Petri nets, including a folding approach that terminates on finite parametric state-class graphs and support for LTL model checking.
-
Dense Integer-Complete Synthesis for Bounded Parametric Timed Automata
Presents parametric extrapolation for dense integer-complete underapproximation of parameter sets in bounded PTAs, with terminating algorithms for reachability and related properties.
-
Weighing Timed Regular Languages: The Final Step (long version)
An algorithm computes the bandwidth of normal timed automata by reducing the problem to finding the maximum reward-to-cost ratio in a weighted finite graph built from the automaton.
-
Learning Alternating Real-Time Automata
AL*RTA learns alternating real-time automata, terminates, and produces smaller models than NL*RTA at the expense of more queries while preserving expressive power.