Re: [tlaplus] Deontic logic with TLA+

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

welcome to this group!

Your description of what you are trying to accomplish does not contain enough details to understand the problem. If it involves modeling the "cloud context" or the "business processes" as algorithms (formally, transition systems), then TLA+ may be very adequate. However, be aware that TLA+ does not have modal operators other than those of temporal logic. You can in principle define the semantics of other modal logics using TLA+ operators (explicitly identifying the set of possible worlds over which the modal operators are evaluated and using operations on sets), and in some cases TLC may be able to evaluate such definitions. Another tool that you might find useful in this context is ProB (http://www.stups.uni-duesseldorf.de/ProB/index.php5/Main_Page), which is based on a constraint solver and also has a TLA+ front-end. However, it is impossible for me to evaluate the suitability of TLA+ and/or these tools without having more information about your problem.

Before embarking on such a "non-standard" use of TLA+, let me advise you to first make sure that you have a clear understanding of what TLA+ is and how one uses it for modeling algorithms and systems. The best starting place for learning about TLA+ is Leslie Lamport's hyperbook, available from http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html.

Hope this helps,

Stephan


On May 14, 2013, at 10:46 AM, noorelh...@xxxxxxxxx wrote:

> Hello!
> This is the first time i use TLA+ I installed it a week ago,the objectif of my work is to formalize some security constraints (cloud context) and validate them with this tool
> for exemaple i've this constraint : colocalisation constraint which aim to group two fragments of business processes in the same cloud 
> 
> i used the deontic logic to formilize this one as follow:
> we have : O ( p^q)=Op^Oq / O:obligation 
> O (Ci (fj)) = impose to put the fragment fj in the cloud ci 
>   colocaliser(f1,f2) :O[Ci(f1^f2)]= O(Ci(f1))^O(Ci(f2))                                                 
> Ci (fj) can read  : the fragment fj is a part of  Cloud Ci
> 
> i've also constraints written in epistemic and doxastic logic,and i don't know how to use this tool to validate this constraints can you help me please ?
> 
> Thank you