Formal Language / Category Theory

[ghasshee]

Smart contracts temporal properties verification

LTL with an “until” operator can specify some interesting properties https://arxiv.org/pdf/1802.06038.pdf (Definition 3.3). Modality of the past is sometimes convenient (if player A has cheated, it can be punished). Or, in Casper contract, other branches are also important (if player A contradicts what it said on another branch). Regarding Coq, the thrid author of the above paper is somebody to contact. You might be interested in modeling Plasma Cash or Plasma MVP They define rather invo…