Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Verified LTL to Buechi Automaton Translation?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Verified LTL to Buechi Automaton Translation?


Chronological Thread 
  • 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.
https://www21.in.tum.de/~lammich/pub/verified_ltl_paper.pdf

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




Archive powered by MHonArc 2.6.18.

Top of Page