Abstract Both hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. This paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories—an extension of answer set programs to the first-order level similar to the way satisfiability modulo theories (SMT) extends propositional satisfiability (SAT). We first show how to represent linear hybrid automata with convex invariants by an action language modulo theories. A further translation into SMT allows for computing them using SMT solvers that support arithmetic over reals. Next, we extend the representation to the general class of non-linear hybrid automata allowing even non-convex invariants. We represent them by an action language modulo ordinary differential equations, which can be compiled into satisfiability modulo ordinary differential equations. We present a prototype systemcplus2aspmtbased on these translations, which allows for a succinct representation of hybrid transition systems that can be computed effectively by the state-of-the-art SMT solverdReal.

We provide reformulations and generalizations of both the semantics of logic programs by Faber, Leone and Pfeifer and its extension to arbitrary propositional formulas by Truszczyński. Unlike the previous definitions, our generalizations refer neither to grounding nor to fixpoints, and apply to firstorder formulas containing aggregate expressions. In the same spirit as the first-order stable model semantics proposed by Ferraris, Lee and Lifschitz, the semantics proposed here are based on syntactic transformations that are similar to circumscription. The reformulations provide useful insights into the FLP semantics and its relationship to circumscription and the first-order stable model semantics.

The advent of emerging technologies such as Web services, service-oriented architecture, and cloud computing has enabled us to perform business services more efficiently and effectively. However, we still suffer from unintended security leakages by unauthorized services while providing more convenient services to Internet users through such a cutting-edge technological growth. Furthermore, designing and managing Web access control policies are often error-prone due to the lack of logical and formal foundation. In this paper, we attempt to introduce a logic-based policy management approach for Web access control policies especially focusing on XACML (eXtensible Access Control Markup Language) policies, which have become the de facto standard for specifying and enforcing access control policies for various applications and services in current Web-based computing technologies. Our approach adopts Answer Set Programming (ASP) to formulate XACML that allows us to leverage the features of ASP solvers in performing various logical reasoning and analysis tasks such as policy verification, comparison and querying. In addition, we propose a policy analysis method that helps identify policy violations in XACML policies accommodating the notion of constraints in role-based access control (RBAC). We also discuss a proof-of-concept implementation of our method called XACMLl2ASP with the evaluation of several XACML policies from real-world software systems.