3 ms·
Ah okay, thanks! The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: Temporal Logic (https://en.wikipedia.or
by pezo1919 7y ago
Ah okay, thanks!
The complexity of Asynchronicity & Concurrency lead me to the formal expression of time related logic: Temporal Logic (https://en.wikipedia.org/wiki/Temporal_logic https://en.wikipedia.org/wiki/Temporal_logic) There are multiple temporal logics with different level of usefulness. (Check Temporal logics section.) I really want to solve harder problems and express deeper relations, so it seems to me what I’d need is CTL at least (https://en.wikipedia.org/wiki/Computation_tree_logic https://en.wikipedia.org/wiki/Computation_tree_logic).
I thought I might want to model my software (any kind of app!) and prove it is working as intended using CTL (or other more expressive TL) in Agda/Idris (Coq/TLA+) and then make a similar implementation in another language.
Eg. there is an LTL implementation in Agda, but I did not find similar things for CTL.(https://github.com/xekoukou/LTL https://github.com/xekoukou/LTL)
What do you think, is it a good idea to express my model using (C)TL in Agda/Idris, or I should use a more dedicated piece of technology for that problem? Is there a limit in case of Agda/Idris for that in theory?
Any resource is appreciated!
- pron 7y agoTLA is also a (linear) temporal logic that's simpler than LTL, and it's at the core of TLA+. If you don't want to spend months studying and then months writing proofs as a learning experience but rather would like to actually specify and verify real systems, use a language with a temporal logic model checker, like TLA+ (that has the TLC model checker) or Promella (Spin). If you want the other kind of experience, there have been implementations of TLA in both Coq and Isabelle.