Generic Property Specification Language (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis (aka LTL for Plug).

In GPSL each property is associated with a named variable. All these variables form the property set Any subset of the property set can be verified during an analysis run.

Assertions: Syntax & Semantics

There are two Boolean constants predefined in the language: true and false

Atomic proposition in GPSL are strings of characters enclosed between pairs of | (ie. | string of characters |). Each atomic proposition can be prefixed with two identifiers specifying the atomic proposition language and the ‘verification’ module on which it should be interpreted.

Boolean Operators

Two expressions f and g can be combined using the following Boolean operators

Operation syntax0 syntax1 syntax2 syntax3 syntax4
negation not f !f ~f    
disjunction f or g f | g f \/ g f + g  
conjunction f and g f & g f && g f /\ g f * g
exclusion f xor g f ^ g      
implication f implies g f -> g f => g    
equivalence f iff g f <-> g f <=> g    

Let Expressions

To simplify the expression of large formula GPSL uses Let expression forms to introduce variables.

    v1 = expr
    v2 = expr
    vn = expr
    v1 op v2

Temporal Logic: Syntax & Semantics

The support for LTL is enabled using LTL3Buchi conversion [1].

Temporal Logic Operators

Two expressions f and g can be combined using the following Boolean operators

operation syntax0 syntax1 syntax2
Next X f next f () f
Eventually F f eventually f <> f
Always G f globally f [] f
Strong Until f U g f until g  
Weak Until f W g    
Weak Release f R g f release g f V g
Strong Release f M g    

Some examples

aliceCS			= |{Alice}1@CS|
bobCS 			= |{Bob}1@CS|
exclusionI 		= []!(|{Alice}1@I| && |{Bob}1@I|)
exclusion  		= []!(aliceCS && bobCS)
eventuallyOneInCS 	= []<>(aliceCS || bobCS)
fairness 		= 
		aliceFlagUP=|{sys}1:flags[0] = true|,
		bobFlagUP=|{sys}1:flags[1] = true|
		 ([]  (  (aliceFlagUP -> (<> aliceCS) )
		      && (bobFlagUP -> (<> bobCS))))  
idling = let
		([]  (!aliceFlagUP -> (![] aliceCS))
		   && (!bobFlagUP -> (![] bobCS)) )
infoften 		=  [] <> bobCS

all = (exclusion & eventuallyOneInCS & fairness & idling)


[1] Babiak, Tomáš, et al. “LTL to Büchi automata translation: Fast and more deterministic.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2012.