mention LTL contrib and Spin operators in README.md

Author: palmskog

README.md

@@ -5,7 +5,9 @@ InfSeqExt
 
 `InfSeqExt` is collection of Coq libraries for reasoning inductively and coinductively on infinite sequences, using modal operators similar to those in linear temporal logic (LTL).
 
-`InfSeqExt` is based on an [earlier library](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5198503) by Deng and Monin. It is intended as a more comprehensive alternative to [`Streams`](https://coq.inria.fr/library/Coq.Lists.Streams.html) in the Coq standard library. In particular, `InfSeqExt` provides machinery commonly used when reasoning about temporal properties of system execution traces. The libraries have some overlap with the less exhaustive [`CTLTCTL`](https://github.com/coq-contribs/ctltctl) Coq contribution, which provides similar machinery. However, in contrast to `CTLTCTL`, `InfSeqExt` does not provide a definition of traces following some labeled reduction relation, nor an explicit notion of time.
+`InfSeqExt` is based on an [earlier library](http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5198503) by Deng and Monin. It is intended as a more comprehensive alternative to [`Streams`](https://coq.inria.fr/library/Coq.Lists.Streams.html) in the Coq standard library. In particular, `InfSeqExt` provides machinery commonly used when reasoning about temporal properties of system execution traces, and follows the modal operator [name conventions](http://spinroot.com/spin/Man/ltl.html) used in the Spin model checker. 
+
+The libraries have some overlap with the less exhaustive [`CTLTCTL`](https://github.com/coq-contribs/ctltctl) and [`LTL`](https://github.com/coq-contribs/ltl) Coq contributions, which provide similar machinery. In contrast to these libraries, `InfSeqExt` does not provide a definition of traces following some labeled reduction relation, nor an explicit notion of time. Fairness is also left up to library users to define.
 
 Requirements
 ------------
@@ -15,7 +17,7 @@ Requirements
 Building
 --------
 
-This project uses [`coqproject.sh`](https://github.com/dwoos/coqproject) for dependency management. To build the libraries, first run `./configure` in the base directory and then run `make`. When added as a dependency to another project using `coqproject.sh`, the namespace is `InfSeqExt`, so Coq files that rely on InfSeqExt will typically include `Require Import InfSeqExt.infseq.`
+This project uses [`coqproject.sh`](https://github.com/dwoos/coqproject) for dependency management. To build the libraries, first run `./configure` in the base directory and then run `make`. When added as a dependency to another project using `coqproject.sh`, the namespace is `InfSeqExt`, so Coq files that rely on the libraries will typically include `Require Import InfSeqExt.infseq.`
 
 infseq
 ------