wsmlVariant _"http://www.wsmo.org/wsml/wsml-syntax/wsml-flight"
namespace { _"http://ip-super.org/ontologies/bro#",
	wsml _"http://www.wsmo.org/wsml/wsml-syntax#",
	dc _"http://purl.org/dc/elements/1.1/" }

ontology _"http://ip-super.org/ontologies/bro#"
     nonFunctionalProperties
          dc#title hasValue "SUPER Behavioural Reasoning Ontology"
          dc#description hasValue "WSML-Flight ontology of the CaSE process algebra"
          dc#publisher hasValue "SUPER European Integrated Project"
          dc#subject hasValue {"process algebra", "behavioural equivalence", "behavioural reasoning"}
          dc#creator hasValue "Barry Norton"
          dc#language hasValue "en-GB"
          dc#date hasValue "$Date: 2007/09/30$"
     endNonFunctionalProperties

	concept Channel 
		nfp
			dc#description hasValue "Channels are used for two-party asymmetric synchronous communications"
		endnfp	

	concept Action
		nfp
			dc#description hasValue "An action is either silent or a communication on a channel."
			dc#relation hasValue {anAction}
		endnfp	
	
	axiom anAction definedBy
		!- ?a memberOf Action and
			?a != silentAction and
			(naf ?a memberOf Input) and
			(naf ?a memberOf Output).
			
	instance silentAction memberOf Action
		nfp
			dc#description hasValue "A silent action is internal step and not the basis of synchronisation."
		endnfp	

	concept Input subConceptOf Action
		nfp
			dc#description hasValue "An input is a blocking wait on a channel until matched by an output on the same channel."
		endnfp	
		hasChannel ofType (1) Channel
		
	concept Output subConceptOf Action
		nfp
			dc#description hasValue "An output is a blocking wait on a channel until matched by an input on the same channel."
		endnfp	
		hasChannel ofType (1) Channel
	
	concept Clock
		nfp
			dc#description hasValue "Clocks are the basis of multi-party symmetric synchronisations subject to maximal progress"
		endnfp	
		
	concept Variable
		nfp
			dc#description hasValue "Variables range over terms and are strictly divided into process term variables and equation term variables"
			dc#relation hasValue {aVariable}
		endnfp	

	axiom aVariable definedBy
		!- ?x memberOf Variable and
		(naf ?t memberOf ProcessVariable) and 
		(naf ?t memberOf EquationVariable).

	concept ProcessVariable subConceptOf Variable
		nfp
			dc#description hasValue "A process variables ranges over process terms by explicit binding."
		endnfp	

	concept EquationVariable subConceptOf Variable
		nfp
			dc#description hasValue "An equation variable refers to a formal variable of an equation system, which is identified by a process and an index, and is indexed within this system."
		endnfp	
		hasProcess ofType (1) ProcessTerm
		hasEquationSystemIndex ofType (1) _integer
		hasIndex ofType (1) _integer
	
	concept Term
		nfp
			dc#description hasValue "Terms defines a behaviour up to free variables and are strictly divided into process terms and equation terms."
			dc#relation hasValue {aTerm, aCaseTerm}
		endnfp	

	axiom aTerm definedBy
		!- ?t memberOf Term and
		(naf ?t memberOf ProcessTerm) and 
		(naf ?t memberOf EquationTerm).

	axiom aCaSETerm definedBy
		!- ?t memberOf Term and
		?t != nil and
		(naf ?t memberOf Prefix) and 
		(naf ?t memberOf Restriction) and
		(naf ?t memberOf Choice) and
		(naf ?t memberOf Parallel) and
		?t != stall and
		(naf ?t memberOf StallClock) and
		(naf ?t memberOf Timeout) and
		(naf ?t memberOf Hiding) and
		(naf ?t memberOf FreeVariable) and
		(naf ?t memberOf VariableBinding).
					
	concept ProcessTerm subConceptOf Term
		nfp
			dc#description hasValue "Process terms define, including subterms that are strictly process terms, behaviour up to variables up to process variables and form processes when all such variables are explicitly bound."
			dc#relation hasValue {aPrefixedProcessTerm, aRestrictedProcessTerm, aChoiceProcessTerm, aParallelProcessTerm, aTimeoutProcessTerm, aHiddenProcessTerm}
		endnfp	

	axiom aPrefixedProcessTerm definedBy
		!- ?p memberOf Prefix and ?p memberOf ProcessTerm and
			?p[hasBody hasValue ?q] and (naf ?q memberOf ProcessTerm).

	axiom aRestrictedProcessTerm definedBy
		!- ?p memberOf Restriction and ?p memberOf ProcessTerm and
			?p[hasSubterm hasValue ?q] and (naf ?q memberOf ProcessTerm).
		
	axiom aChoiceProcessTerm definedBy
		!- ?p memberOf Choice and ?p memberOf ProcessTerm and
			?p[hasSubterm hasValue ?q] and (naf ?q memberOf ProcessTerm).

	axiom aParallelProcessTerm definedBy
		!- ?p memberOf Parallel and ?p memberOf ProcessTerm and
			?p[hasSubterm hasValue ?q] and (naf ?q memberOf ProcessTerm).

	axiom aFreeVariableProcessTerm definedBy
		!- ?p memberOf FreeVariable and ?p memberOf ProcessTerm and
			?p[hasVariable hasValue ?v] and (naf ?v memberOf ProcessVariable).
			
	axiom aTimeoutProcessTerm definedBy
		!- ?p memberOf Timeout and ?p memberOf ProcessTerm and
			?p[hasLeftTerm hasValue ?q] and ?p[hasRightTerm hasValue ?r] and
			(naf ?q memberOf ProcessTerm) or (naf ?r memberOf ProcessTerm).

	axiom aHiddenProcessTerm definedBy
		!- ?p memberOf Hiding and ?p memberOf ProcessTerm and
			?p[hasSubterm hasValue ?q] and (naf ?q memberOf ProcessTerm).
			
	concept EquationTerm subConceptOf Term
		nfp
			dc#description hasValue "Equation terms define, including subterms that are strictly equation terms, behaviour up to free variables that map to the formal variables of the containing equation system rather than being explicitly bound in the term."
			dc#relation hasValue {anEquationTerm, aPrefixedEquationTerm, aRestrictedEquationTerm, aChoiceEquationTerm, aTimeoutEquationTerm, aParallelEquationTerm, aHiddenEquationTerm}
		endnfp	

	axiom anEquationTerm definedBy
		!- ?e memberOf EquationTerm and ?e memberOf ProcessVariable.

	axiom aPrefixedEquationTerm definedBy
		!- ?e memberOf Prefix and ?e memberOf EquationTerm and
			?e[hasBody hasValue ?f] and (naf ?f memberOf EquationTerm).

	axiom aRestrictedEquationTerm definedBy
		!- ?e memberOf Restriction and ?e memberOf EquationTerm and
			?e[hasSubterm hasValue ?f] and (naf ?f memberOf EquationTerm).

	axiom aChoiceEquationTerm definedBy
		!- ?e memberOf Choice and ?e memberOf EquationTerm and
			?e[hasSubterm hasValue ?f] and (naf ?f memberOf EquationTerm).

	axiom aParallelEquationTerm definedBy
		!- ?e memberOf Parallel and ?e memberOf EquationTerm and
			?e[hasSubterm hasValue ?f] and (naf ?f memberOf EquationTerm).

	axiom aFreeVariableEquationTerm definedBy
		!- ?e memberOf FreeVariable and ?e memberOf EquationTerm and
			?e[hasVariable hasValue ?v] and (naf ?v memberOf EquationVariable).

	axiom aTimeoutEquationTerm definedBy
		!- ?e memberOf Timeout and ?e memberOf EquationTerm and
			?e[hasLeftTerm hasValue ?f] and ?e[hasRightTerm hasValue ?g] and
			(naf ?f memberOf EquationTerm) or (naf ?g memberOf EquationTerm).
			
	axiom aHiddenEquationTerm definedBy
		!- ?e memberOf Hiding and ?e memberOf EquationTerm and
			?e[hasSubterm hasValue ?f] and (naf ?f memberOf ProcessTerm).

	instance nil memberOf {ProcessTerm, EquationTerm}
		nfp
			dc#description hasValue "Nil is the inactive behaviour, i.e. the one which engages in no communications and have no effect on the progress of time."
		endnfp	
	
	concept Prefix subConceptOf Term
		nfp
			dc#description hasValue "A prefix defines that the first step in a behaviour is a given action, a body defines the remainder of the behaviour."
		endnfp	
		hasAction ofType (1) Action
		hasBody ofType (1) Term

	concept Restriction subConceptOf Term
		nfp
			dc#description hasValue "A resticted term defines a behaviour according to its subterm, but removing behaviours starting with communications on any of the restricted channels."
		endnfp	
		hasSubterm ofType (1) Term
		hasChannel ofType (1 *) Channel

	concept Choice subConceptOf Term
		nfp
			dc#description hasValue "A choice defines a behaviour in which the first step is a non-deterministic choice between the behaviour of two subterms, according to whichever performs an action first."
		endnfp	
		hasSubterm ofType (1 *) Term
	
	concept Parallel subConceptOf Term
		nfp
			dc#description hasValue "A parallel term defines a behaviour according to the concurrent interaction of the behaviours defined by its subterms."
		endnfp	
		hasSubterm ofType (1 *) Term

	instance stall memberOf {ProcessTerm, EquationTerm}
		nfp
			dc#description hasValue "Stall is a neglible time behaviour, i.e. it engages in no communications but allows time to pass on no visible clock."
		endnfp	
	
	concept StallClock subConceptOf {ProcessTerm, EquationTerm}
		nfp
			dc#description hasValue "For each clock there is a specific stalling behaviour that affects no other clock."
		endnfp	
		hasClock ofType (1) Clock

	concept Hiding subConceptOf Term
		nfp
			dc#description hasValue "A term with a hidden clock defines a behaviour according to its subterm but re-labels ticks of that clock to silent actions."
		endnfp
		hasSubterm ofType (1) Term
		hasClock ofType (1) Clock
					
	concept Timeout subConceptOf Term
		nfp
			dc#description hasValue "A timeout defines a behaviour according to one (left) subterm unless the clock specified is allowed to tick, in which case it proceeds as per the other (right) subterm.  Timeouts are strictly either fragile or stable."
			dc#relation hasValue {aTimeout1, aTimeout2}
		endnfp	
		hasLeftTerm ofType (1) Term
		hasClock ofType (1) Clock
		hasRightTerm ofType (1) Term

	axiom aTimeout1 definedBy
		!- ?t memberOf Timeout and
		(naf ?t memberOf FragileTimeout) and 
		(naf ?t memberOf StableTimeout).
	
	axiom aTimeout2 definedBy
		!- ?t memberOf FragileTimeout and 
		?t memberOf StableTimeout.

	concept FragileTimeout subConceptOf Timeout
		nfp
			dc#description hasValue "In a fragile timeout other clocks allowed by the left subterm will break the timeout handler."
		endnfp	
		
	concept StableTimeout subConceptOf Timeout
		nfp
			dc#description hasValue "In a stable timeout other clocks allowed by the left subterm will not break the timeout handler."
		endnfp	
		
	concept FreeVariable subConceptOf Term
		nfp
			dc#description hasValue "A term with a free variable defers the definition of the behaviour to whatever term is later bound to the variable."
		endnfp	
		hasVariable ofType (1) Variable

	concept VariableBinding subConceptOf ProcessTerm
		nfp
			dc#description hasValue "A process term may explicitly bind a variable to its subterm, which may include that variable so allowing recursion."
		endnfp	
		bindsVariable ofType (1) ProcessVariable
		hasBody ofType (1) ProcessTerm


	relation EquationSystem (ofType ProcessTerm, ofType _integer, ofType _integer, ofType EquationTerm)
		nfp
			dc#description hasValue "A equation system is an indexed set of equation terms.  This relation contains all equation systems, themselves indexed by a process term and integer (so that several equation systems can be defined for each process term)."
			dc#relation hasValue {directEquationSystem, normalisingEquationSystems}
		endnfp	


	relation StrongCongruence (ofType ProcessTerm, ofType ProcessTerm) subRelationOf TemporalObservationCongruence
		nfp
			dc#description hasValue "Strong congruence relates those process terms between which a (strong) bisimulation exists."
			dc#relation hasValue {aStrongCongruence}
		endnfp	
	
	relation TemporalObservationCongruence (ofType ProcessTerm, ofType ProcessTerm) subRelationOf WeakEquivalence
		nfp
			dc#description hasValue "Temporal observation congruence is the largest relation between process terms within weak equivalence which is a congruence."
			dc#relation hasValue {aTemporalObservationCongruence}
		endnfp	
	
	relation WeakEquivalence (ofType ProcessTerm, ofType ProcessTerm)
		nfp
			dc#description hasValue "Weak equivalence relates those process terms between which a weak bisimulation exists."
			dc#relation hasValue {aWeakEquivalence}
		endnfp