State exploration is done in a way that all possible execution combinations are searched. Execution combinations determined by the conditions of actions

Ambient Logic formulas are decomposed as the the temporal operators are at the top of the parse tree of the formula 

Our model checking proach is a derived, extended form of mardere.

In our scope of project we are not dealing with state explosion problem.


Ambient calculus
	in our ambient calculus input and output operators are constraint that only names are 
	applicable to input and output operators

	we do not support atomic process in our ambient calculus.
	
	n our calculus we take names a identifiers. i.e. they must be unique
	
   
   
Ambient Logic
	In our ambient logic we do not support atomic formulas 
	
	our ambient logic includes only not and or operations due to other propositional logic elements are derivable 
	
	