coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mario Alvarez <mmalvare AT eng.ucsd.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Verified LTL to Buechi Automaton Translation?
- Date: Thu, 20 Apr 2017 11:56:35 -0700
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mmalvare AT eng.ucsd.edu; spf=Pass smtp.mailfrom=mmalvare AT eng.ucsd.edu; spf=None smtp.helo=postmaster AT mail-wr0-f178.google.com
- Ironport-phdr: 9a23:jiESqhOrG7zQVF+TGV0l6mtUPXoX/o7sNwtQ0KIMzox0Lf/6rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5u7YYQVFeoBPOFYpJThqlsKsxuxHxOsC/3uyzRVgXL22Kg63P4lEQHYxgMgBcwBvW/Ko9XzO6ceS/21w7XTzTredf9Zxyry6JXRfx0nvPqCXqpwfNLPxUUzEw7JlFadpIz/Mz+IyOgAsHKX4/diWO+sk2IqqQ58riKyyssyioTFnIEYxk7e+Sh2z4s4I8CzRlRhbt6+CpRQsjmXN4toTcMmRGFloCM6xacHuZ6/ZSQLxo4nywLGZ/yJboSF4BHuWPyeITd/g3Jld7a/iAio/Ue8ze38U9G40FdMriVbjtnBrm4B2wDX58SdSfZw/l2t1SuR2w3Q8O1IPEI5mKnDJ54k2LEwl54TsUrZHi/xnUX7lKqWdkA+9eis9eToeK/mqYGHOoBqjAH+Pb4imtGjDuQjLwcCRXaU9vmh1LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mPVW/ZNTQpgFPvvpV1254NndBxsnOha56+vhB5Ng3ZgSH2+DH/nKY+vprVaU67d3cKG3b4gPtWOlJg==
Hi Coq Club,
Are there any Coq developments that you know of where the translation from LTL formulas to their corresponding Buechi Automata is implemented and verified? I'm curious about implementing a model checker in Coq, and this seems like a useful component to build off, if it exists.
Best,
Mario
- [Coq-Club] Verified LTL to Buechi Automaton Translation?, Mario Alvarez, 04/20/2017
- Re: [Coq-Club] Verified LTL to Buechi Automaton Translation?, Van Chan Ngo, 04/20/2017
Archive powered by MHonArc 2.6.18.