Scribd
Upload
245 views11 pages

Agents Based On Propositional Logic

Model checking is a verification method used to determine if a model meets its specifications by exploring all possible states. It employs techniques like symbolic model checking, Boolean Satisfiability (SAT) solvers, and Binary Decision Diagrams (BDDs), and is applied in AI for verifying knowledge representation, reasoning, and planning. Real-world applications include ensuring the correctness of traffic light systems and the behavior of autonomous vehicles.

Uploaded by

hegdeanisha0
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF or read online on Scribd
245 views11 pages

Agents Based On Propositional Logic

Model checking is a verification method used to determine if a model meets its specifications by exploring all possible states. It employs techniques like symbolic model checking, Boolean Satisfiability (SAT) solvers, and Binary Decision Diagrams (BDDs), and is applied in AI for verifying knowledge representation, reasoning, and planning. Real-world applications include ensuring the correctness of traffic light systems and the behavior of autonomous vehicles.

Uploaded by

hegdeanisha0
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF or read online on Scribd
You are on page 1/ 11
What is Model Checking? ¢ Introduce model checking as a method to verify if a model (e.g., a system, algorithm) meets its specifications. ? e Explain how it works by systematically exploring all possible states of the model. ? Ill. Model Checking Algorithms * Symbolic Model Checking: © Explain how symbolic model checking uses efficient algorithms to explore the state space of a model. © Introduce techniques like Boolean Satisfiability (SAT) solvers and Binary Decision Diagrams (BDDs). * Model Checking Tools: © Mention popular model checking tools like NuSMV, SPIN, and others. * Model Checking in Al Applications: © Discuss how model checking can be used to verify the correctness of Al systems, such as: = Knowledge Representation: Ensuring that knowledge bases are consistent and complete. Reasoning: Verifying that inference rules lead to correct conclusions. Planning: Checking if plans are feasible and lead to desired goals. & Simple Examples: e Use simple examples to illustrate the concepts of propositional logic and model checking. ¢ For example, a simple robot navigation problem where model checking can verify if the robot can reach its destination. Real-World Applications: ¢ Discuss real-world applications of model checking in Al, such as: * Verifying the correctness of traffic light control systems. * Checking the behavior of autonomous vehicles. « Ensuring the reliability of critical systems. @ Effective Propositional Model Checking Agent -> Cleaning Agent -> Clean Dining Table Rules -> Open the arms cleaning Close the arms -> Vase! # Define propositions (statements about the robot) near_vase = True # Is the robot near the vase? arms_extended = True # Are the robot's arms extended? # Safety rule (formula) - We want to avoid arms being extended near the \ safe_B@Si0n = not (near_vase and arms_extended) # Print the safety check if safe_action: print("Robot is safe: Arms not extended near the vase!") else: print("Warning! Robot arms might knock over the vase. Be careful!") 7.7: Agents Based on Propositional Logic « For WumpusWorld: - the agent needs to deduce the world given percepts. - we need a complete logic model - we need agent to keep track of the world - we need the agent to make plans The current state of the world + The KB is used by the agent for deducing what to do. k * The KB has axioms and percept sentences from agent experiences. « Axioms are sentences. * Started listing them earlier. * Example axioms: - (>P,,) ; starting square has no pit. - ((W,,,); and no wumpus - B,, = (P,, VP, ) ; breezy iff neighbor has pit - S,,(W,,VW,,) | smelly iff neighbor has Wumpus - Exactly one Wumpus: + atleast one: W,, VW,,V- VW,, VW, * at most one + What about percepts? - Take time into consideration. - On turn 3, no stench? Add 7Stench’ to the ~ On turn 4, stench? Add Stench* to the KB. = The time-proposition relationship works for any part of the changing world. «+ Initial KB has L°, , has agent in 1,1 on turn 0. - Apart of the world that changes is said to be fluent. (a state variable) - Permanent aspect without needing a “time stamn® are nallad atamnncal senelablne - For all pairs of squares, one has to have no Wumpus: mW, ¥V Wi2 WW, VWs WW, v Wis ®

You might also like