Using TLC to model check "rule-based expert systems"

[Jay Parlar]

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.

[Stephan Merz]

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

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Jay Parlar]

On Tuesday, 30 April 2019 12:42:14 UTC-4, Stephan Merz wrote:

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.

I have the same worries about state space (even if I were to do some "smart" things to limit it), and I've also been thinking that constraint solving might be the right approach. Thanks for helping give confidence to my thoughts!

Jay P.

[Ron Pressler]

I have a specification using a style called "behavioral programming" intended just for this kind of specification, as an interaction of rules: https://pron.github.io/files/TicTacToe.pdf

[Jay Parlar]

Thanks, I’ll take a closer look tomorrow. Does this have some mechanism for detecting inconsistent/conflicting rules?

[Ron Pressler]

I believe conflicting rules would either result in no behaviors (equivalent to FALSE, i.e. you can verify Spec => FALSE) or in a deadlock, which you can detect with liveness. But the main idea is to express the specification not as a state machine, but as a conjunction of state machines, each corresponding to a rule ("conjoined specifications"). Not generally recommended, but might be useful.

[Morgan Weetman]

I studied expert systems informally 20 years ago so take this with a grain of salt, but from memory the systems decisions would develop various weights based on training. In an expert system a human assists (trains) the system when a decision is incorrect or not preferable.

The system you described seems more like a complex classification system if you can add rules as you go. 

This doesn't really answer your question sorry...but I think others have already done so.

--

[Chris Ortiz]

Hi Ron,

Thank you for that example. That TicTacToe really helps me in understanding another way of composing specs in iterative manner, which I think is really valuable in real life spec composition.

I have 1 comment. I am not sure if it is a typo or not. When I tried it in TLC it is still ok though. In your PDF you have a definition below:

TicTacToe6 ∆= TicTacToe4 ∧ MarkCenterIfAvailable 

Should it be?

TicTacToe6 ∆= TicTacToe5 ∧ MarkCenterIfAvailable  

Thanks,

Zitro