Scribd
Upload
271 views4 pages

Propositional Model Checking in Python

The document outlines a Python implementation of a propositional model-checking algorithm that verifies the truth of Boolean expressions under various truth assignments. It details the steps for identifying variables, generating truth assignments, evaluating expressions, and classifying the formula as a tautology, satisfiable, or contradiction. An example usage of the program demonstrates its functionality and outputs a truth table along with the classification result.

Uploaded by

Saranya S - AP - CSE
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as DOCX, PDF, TXT or read online on Scribd
271 views4 pages

Propositional Model Checking in Python

The document outlines a Python implementation of a propositional model-checking algorithm that verifies the truth of Boolean expressions under various truth assignments. It details the steps for identifying variables, generating truth assignments, evaluating expressions, and classifying the formula as a tautology, satisfiable, or contradiction. An example usage of the program demonstrates its functionality and outputs a truth table along with the classification result.

Uploaded by

Saranya S - AP - CSE
Copyright
© All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as DOCX, PDF, TXT or read online on Scribd

Propositional Model Checking using Python

Aim

To implement a simple propositional model-checking algorithm using Python that verifies


whether a given propositional formula is true under different truth assignments.

Algorithm for Propositional Model Checking

Input:

A Boolean expression with propositional variables (e.g., "(p or q) and (not p or q)").

Steps:

1. Identify Variables:
o Extract all unique propositional variables (p, q, r, ...) from the given Boolean
expression.
2. Generate Truth Assignments:
o Create all possible combinations of True and False values for the extracted
variables.
3. Evaluate Expression:
o Substitute each truth assignment into the Boolean expression.
o Compute the truth value using Python's eval() function.
4. Output Truth Table:
o Display all possible truth assignments along with the corresponding evaluation
results.
5. Classify the Formula:
o If the formula is True for all truth assignments → Tautology.
o If the formula is True for at least one truth assignment but not all → Satisfiable
but not a Tautology.
o If the formula is False for all truth assignments → Contradiction.
6. Output the Final Result.

Program:
from itertools import product
# Function to evaluate a Boolean expression under a given truth assignment
def evaluate_expression(expression, variables, values):
env = dict(zip(variables, values)) # Map variables to their truth values
return eval(expression, {}, env) # Evaluate the expression using the assigned values

# Function to perform propositional model checking


def propositional_model_check(expression):
valid_vars = {'p', 'q', 'r'} # Define valid propositional variables
variables = sorted(set(c for c in expression if c in valid_vars)) # Extract unique variables
truth_assignments = list(product([False, True], repeat=len(variables))) # Generate truth table
assignments

results = [evaluate_expression(expression, variables, assignment) for assignment in


truth_assignments]

# Display the Truth Table


print("Truth Table:")
print(" | ".join(variables) + " | Result")
print("-" * (len(variables) * 4 + 9))
for assignment, result in zip(truth_assignments, results):
print(" | ".join(str(int(val)) for val in assignment) + f" | {int(result)}")

# Determine the classification of the Boolean formula


if all(results):
return "The formula is a Tautology (always True)."
elif any(results):
return "The formula is Satisfiable but not a Tautology."
else:
return "The formula is a Contradiction (always False)."

# Example Usage
expression = "(p or q) and (not p or q)" # Example Boolean formula
result = propositional_model_check(expression)
print("\nResult:", result)

Output

Truth Table:
p | q | Result
-------------------
0|0| 0
0|1| 1
1|0| 1
1|1| 1

Result: The formula is Satisfiable but not a Tautology.

Result:

Thus the program to implement Propositional Model checking Algorithm is implemented and

executed successfully.

Common questions

Powered by AI

The algorithm uses the itertools.product function to generate all possible truth assignments for the extracted propositional variables. This method creates a Cartesian product of True and False values, repeating the number of times equal to the number of unique variables extracted from the expression. This ensures comprehensive coverage of all possible combinations of truth values, allowing for complete evaluation of the expression against every possible assignment .

The classification process in the Python program uses a straightforward evaluative approach: after generating and evaluating all truth assignments, it checks the results. If all results are True, the formula is classified as a tautology. If at least one result is True, it is classified as satisfiable but not a tautology. If all results are False, the formula is classified as a contradiction. This classification mechanism allows the program to determine the logical status of the formula comprehensively .

A Boolean formula is classified as a tautology if it returns True for all possible truth assignments, indicating it is always true. It is considered satisfiable but not a tautology if it is True for at least one truth assignment but not all, meaning there is some condition under which it holds. It is classified as a contradiction if it returns False for all possible truth assignments, indicating there is no condition under which it is true .

The 'evaluate_expression' function works by mapping propositional variables to their truth values using a dictionary. It then evaluates the given expression under the specified truth assignment using Python's eval() function. The inputs to the function are the Boolean expression, a list of variables, and a corresponding list of values. The function returns the truth value (True or False) of the evaluated expression .

The steps involved in implementing a simple propositional model-checking algorithm using Python include: 1) identifying variables by extracting all unique propositional variables from the given Boolean expression; 2) generating truth assignments by creating all possible combinations of True and False values for the extracted variables; 3) evaluating the expression by substituting each truth assignment into the Boolean expression and computing the truth value using Python's eval() function; 4) outputting a truth table that displays all possible truth assignments along with the corresponding evaluation results; 5) classifying the formula based on the evaluation results as a tautology, satisfiable but not a tautology, or a contradiction; and 6) outputting the final result .

Extracting all unique propositional variables from a given Boolean expression is crucial because it determines the number of dimensions across which truth values need to be evaluated. Each unique variable represents a dimension of possible truth assignments, and failing to identify them accurately might lead to incomplete or incorrect truth assignment generation, thus affecting the model checking result validity .

The itertools.product function is used to create a Cartesian product of True and False values repeated for the length of the list of unique variables. This means it generates all possible combinations of these two truth values, which is necessary to evaluate the expression across all potential truth conditions. The function effectively enumerates all permutations needed to check logical formulas comprehensively .

The 'propositional_model_check' function is central to verifying a Boolean formula by orchestrating the steps of identifying variables from the expression, generating all truth assignments using itertools.product, evaluating the expression against each assignment using the 'evaluate_expression' function, and finally determining and returning the classification of the formula (tautology, satisfiable, or contradiction) based on the evaluation results .

The result of propositional model checking is displayed by printing a truth table that shows all possible truth assignments along with their corresponding evaluation results. Additionally, based on the evaluation of truth assignments, a conclusion about whether the formula is a tautology, satisfiable but not a tautology, or a contradiction is printed to convey the findings clearly and effectively .

The eval() function contributes significantly to the propositional model-checking algorithm by dynamically evaluating the Boolean expression based on the current context of truth assignments. The function interprets and executes the expression string as a Python expression, enabling the determination of its truth value appropriately in each context. This dynamic execution allows for a flexible and comprehensive evaluation of all permutations generated by the truth assignment process .

You might also like