Timed Automata Verification and Synthesis Via Finite Automata Learning
Copyright policy )Timed Automata Verification and Synthesis Via Finite Automata Learning
AbstractWe present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. We use automata learning algorithms to learn finite automata approximations of the timed automaton component, in order to reduce the problem at hand to finite-state model checking or to finite-state controller synthesis. We present an experimental evaluation of our approach.
Automaton, Specification and verification (program logics, model checking, etc.), Semi-Supervised Learning, Automata Theory and Formal Languages, Finite Automata, Runtime Verification, Formal languages and automata, Synchronizing Automata, [INFO] Computer Science [cs], Theoretical computer science, Artificial Intelligence, Temporal Logic, Quantum finite automata, automata learning, Active Learning in Machine Learning Research, Automata theory, Finite-state machine, compositional verification, Computational learning theory, Computer science, model checking, Programming language, Timed automaton, Computational Theory and Mathematics, timed automata, Computer Science, Physical Sciences, assume guarantee reasoning, Formal Methods in Software Verification and Control
Automaton, Specification and verification (program logics, model checking, etc.), Semi-Supervised Learning, Automata Theory and Formal Languages, Finite Automata, Runtime Verification, Formal languages and automata, Synchronizing Automata, [INFO] Computer Science [cs], Theoretical computer science, Artificial Intelligence, Temporal Logic, Quantum finite automata, automata learning, Active Learning in Machine Learning Research, Automata theory, Finite-state machine, compositional verification, Computational learning theory, Computer science, model checking, Programming language, Timed automaton, Computational Theory and Mathematics, timed automata, Computer Science, Physical Sciences, assume guarantee reasoning, Formal Methods in Software Verification and Control
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).3 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Top 10% influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!