FL is correct that it's easy to encode an SOS semantics in TLA+. But
if you're talking about a real language with concurrency, I'd be
surprised if it has an SOS semantics. For example, in Java, if b is a
boolean variable that can be accessed by multiple threads, I have no
idea what the meaning is of the statement
b = ! b ;
If the people who designed the semantics of Java did anything like the
designers of two memory systems I've looked at--Alpha and Itanium--the
semantics is quite complicated, almost impossible to understand,
and unlikely to be describable with SOS.
Leslie