Re: [tlaplus] Using TLC to model check "rule-based expert systems"

[Stephan Merz <stephan.merz@xxxxxxxxx>]

I don't have any experience with expert systems, but I guess in principle what you suggest should be possible. I am a bit afraid, though, about TLC being overwhelmed with the state space, and I'd consider using constraint solving for finding values that match guards of different rules and then explore the actions of these rules.

Stephan

> On 30 Apr 2019, at 16:10, Jay Parlar <parlar@xxxxxxxxx> wrote:
> 
> A group of folks at work came to me with an interesting question:
> 
> They have a "rule based expert system" (see http://sce2.umkc.edu/csee/leeyu/class/CS560/Lecture/lect-rule1.pdf as an example). A piece of data comes into the system, and it's pipelined/filtered through potentially hundreds of matching and prioritized rules, coming out the other side as possibly modified by the actions in the rules.
> 
> Because there are so many rules, it's often a problem when a new rule is proposed for the system. It's hard for any human to know all the rules that are present, so it's hard to know if a new rule will "conflict" with an existing rule. And if so, for which conditions would it conflict?
> 
> The question was: Would it be possible to translate the rules into TLA+, and have TLC check to see if the addition of a new rule would conflict with existing rules?
> 
> I have zero background with expert systems, and I haven't yet come across a general solution to this. When the literature mentions "conflict resolution", it appears to be runtime-based, when the expert system finds two rules with matching conditions for a particular piece of data. I'd like to use TLC to do that beforehand, to explore the state space of potential inputs and see if any would cause conflicts when a new rule is added. I had one theory about doing this via refinement, but it quickly fell apart when reasoning about a new rule introducing "desired changes" vs "undesired/unexpected changes".
> 
> Is this a ridiculous thought? Has anyone tried something like this, or does someone with knowledge system expertise think this is even feasible?
> 
> Thanks,
> Jay P.
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.