<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>