[Agda] TLA+ or LTL in agda ?

Setzer A.G.

2018-06-06 22:59:03 UTC

bashar and myself have implemented process algebras in CSP in Agda. We haven't implemented LTL but that research is related.

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) https://github.com/kazkansouh/agda ) 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.

Anton

________________________________
From: Agda <agda-***@lists.chalmers.se> on behalf of Ulf Norell <***@gmail.com>
Sent: 05 June 2018 05:34:22
To: Apostolis Xekoukoulotakis
Cc: agda list
Subject: Re: [Agda] TLA+ or LTL in agda ?

Liam O'Connor's Applications of Applicative Proof Search [1] might be relevant.

/ Ulf

[1] https://scholar.google.se/scholar?hl=en&as_sdt=0%2C5&q=Applications+of+applicative+proof+search&btnG=

On Tue, Jun 5, 2018 at 6:06 AM, Apostolis Xekoukoulotakis <***@gmail.com<mailto:***@gmail.com>> wrote:
Has anyone thought of implementing tla+ in Agda?

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.

I would like to express in LTL and agda , the Dining Philosophers' problem or Paxos.

Apart from Alan , has anyone else worked on LTL in agda?