LTL with arithmetic and its applications in reasoning about hierarchical systems

DOI10.29007/WPG3MaRDI QIDQ5222965zbMATH OpenOpenAlexFDO

Authors Rachel Faran, Orna Kupferman

Publication date 4 July 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.29007/wpg3

zbMATH Keywords

integer linear programmingmodel checkinghierarchical systemsinfinite alphabetsLTL with arithmetic

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Improved model checking of hierarchical systems
• Improved model checking of hierarchical systems
• Extending temporal logics with data variable quantifications
• Taming past LTL and flat counter systems
• Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints

Cited in

(4)

• SEPARATING AUXILIARY ARITY HIERARCHY OF FIRST-ORDER INCREMENTAL EVALUATION SYSTEMS USING (3K+1)-ary INPUT RELATIONS
• Realizability modulo theories
• On synthesis of specifications with arithmetic
• Boolean abstractions for realizability modulo theories

This page was built for publication: LTL with arithmetic and its applications in reasoning about hierarchical systems

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