Superposition-based analysis of first-order probabilistic timed automata

DOI10.1007/978-3-642-16242-8_22MaRDI QIDQ4933313zbMATH OpenOpenAlexFDO

Authors Arnaud Fietzke, Holger Hermanns, Christoph Weidenbach

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_22

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Recommendations

• Superposition as a decision procedure for timed automata
• Model checking for probabilistic timed automata
• \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper)
• Stochastic games for verification of probabilistic timed automata
• Symbolic model checking for probabilistic timed automata

Cited in

(3)

• Superposition as a decision procedure for timed automata
• Superposition decides the first-order logic fragment over ground theories
• A survey of timed automata for the development of real-time systems

Describes a project that uses

Uses Software

• MoDeST

This page was built for publication: Superposition-based analysis of first-order probabilistic timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4933313)