coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Van Chan Ngo <chan.ngo2203 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Verified LTL to Buechi Automaton Translation?
- Date: Thu, 20 Apr 2017 16:49:01 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chan.ngo2203 AT gmail.com; spf=Pass smtp.mailfrom=chan.ngo2203 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f177.google.com
- Ironport-phdr: 9a23:oBG0ZBE6WbXp8z3tvQCEWJ1GYnF86YWxBRYc798ds5kLTJ78ocWwAkXT6L1XgUPTWs2DsrQf2raQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4l/27Yl8J+gqxbrgyjqBJ8xIDZe5uaOOZ7fq7HfdMWWXRNU8BMXCJBGIO8aI4PAvIOMulCqYn2ukUDrRukCgmqGejh0jBIhnjr1qA9z+shERvJ3Ao6E9IIv3TUq8v5OLkOXe2716TIwjDDYOlX2Tf58oTHbhchofSVUL92bMHfx04vFwbfgVWRr4zoJy+V1vkIs2SB8uVvS+SigHMkpQFpujWj2Nsgh43Tio8Wyl3I7zt1zJs0KNGiVUJ2Y9ypHINNuy2ENIZ6WN0uTm9qtSog17ELupG2cDIWxJkh2hXRceaIc5KS7RLmTOuRISl3hHZieL+ngha960mgyunlWsmtzFZGsjNJktfRun0P1RHf8MeHSvx6/keu3TaAyRrf5f1DIUAxjabbKpghzaAslpcLr0jPAiv7lF/1gaKWbEko5PWk5uX9brn7pJKRNZd4igTkPaQvnsy/D/44Mg8LX2WD5eu81Kfs/UvjTLVMgf02lbfVvI7GKckVvaO5DApV3Zwi6xa7FTupzNMYnXwfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfbsuFnAzeImJaGqa4hd7D39Iv5j4fHp1yVhwncSeKCo2d0cb3XuTacuGFmQfXe52oRJKmwNpAdrFOE=
Hi,
I know there exists an implementation of LTL model checker in Isabelle. It think these techniques might be used for Coq.
Best,
-Chan
On Apr 20, 2017, at 2:56 PM, Mario Alvarez <mmalvare AT eng.ucsd.edu> wrote: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.