SMT-based synthesis of distributed systems | Zendy

Bernd Finkbeiner | Zendy; Sven Schewe | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

SMT-based synthesis of distributed systems

Author(s) -

Bernd Finkbeiner,

Sven Schewe

Publication year - 2007

Publication title -

citeseer x (the pennsylvania state university)

Language(s) - English

Resource type - Conference proceedings

DOI - 10.1145/1345169.1345178

Subject(s) - computer science , satisfiability , automaton , satisfiability modulo theories , simple (philosophy) , arbiter , boolean satisfiability problem , theoretical computer science , solver , finite state machine , quantifier (linguistics) , algorithm , parallel computing , programming language , philosophy , epistemology , artificial intelligence

We apply SMT solving to synthesize distributed systems from specifications in linear-time temporal logic (LTL). The LTL formula is translated into an equivalent universal co-Büchi tree automaton. The existence of a finite transition system in the language of the automaton is then specified as a quantified formula in the theory (N,

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research