Multi-valued Logic for Static Analysis and Model Checking

We extend Alternation-Free Least Fixed Point Logic to be based on Belnap logic, while maintaining the close correspondence between static analysis and model checking pioneered by Bernhard Steffen, and opening up for handling access control policies central to the construction of secure IT systems.