<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Helvetica,sans-serif;" dir="ltr">
<p style="margin-top:0;margin-bottom:0">bashar and myself have implemented process algebras in CSP in Agda. We haven't implemented LTL but that research is related.</p>
<p style="margin-top:0;margin-bottom:0">Furthermore Karim Kanso integrated model checking (CTL) into Agda. It wasn't taken over into main Agda but it could still be integrated (there is a git repository (sorry github)
<a href="https://github.com/kazkansouh/agda" class="OWAAutoLink" id="LPlnk229087" previewremoved="true">
https://github.com/kazkansouh/agda</a> ) He implemented a (not very efficient) model checker for CTL which was then overriden by calls to a model checker, so that the whole thing is efficient.</p>
<p style="margin-top:0;margin-bottom:0"><br>
</p>
<p style="margin-top:0;margin-bottom:0">Anton<br>
</p>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Ulf Norell <ulf.norell@gmail.com><br>
<b>Sent:</b> 05 June 2018 05:34:22<br>
<b>To:</b> Apostolis Xekoukoulotakis<br>
<b>Cc:</b> agda list<br>
<b>Subject:</b> Re: [Agda] TLA+ or LTL in agda ?</font>
<div> </div>
</div>
<meta content="text/html; charset=utf-8">
<div>
<div dir="ltr">
<div>Liam O'Connor's Applications of Applicative Proof Search [1] might be relevant.<br>
</div>
<div><br>
</div>
<div>/ Ulf<br>
</div>
<div><br>
</div>
<div>[1] <a href="https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=">
https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=</a></div>
</div>
<div class="x_gmail_extra"><br>
<div class="x_gmail_quote">On Tue, Jun 5, 2018 at 6:06 AM, Apostolis Xekoukoulotakis
<span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br>
<blockquote class="x_gmail_quote" style="margin:0 0 0 .8ex; border-left:1px #ccc solid; padding-left:1ex">
<div dir="ltr">
<div>Has anyone thought of implementing tla+ in Agda?<br>
</div>
<div><br>
</div>
<div>I found Alan Jeffrey's Linear Temporal Logic written in Agda but there is no mention of concurrency, so I am unsure if LTL is sufficient for concurrency.<br>
</div>
<div><br>
</div>
<div><br>
</div>
<div>I would like to express in LTL and agda , the Dining Philosophers' problem or Paxos.</div>
<div><br>
</div>
<div>Apart from Alan , has anyone else worked on LTL in agda?<br>
</div>
</div>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
<br>
</div>
</div>
</body>
</html>