Hi there,
Structural operational semantics (SOS) [1] is a formal method to specify the semantics of a programming language esp. at runtime
using transition systems for program state.
Suppose that for programming language L, there exists an SOS spec. One of the main features of L is concurrency.
I am wondering and curious if TLA+ can be used to specify such a programming language, and thus the runtime
that a running programming in L would create. The goal is to be able to prove/disprove certain properties of the runtime
of the language in regards with concurrency, such as dead locks or live locks.
I am very new to TLA so excuses if the question lacks certain prerequisites.
Thanks,
Behrooz