We extend (type-2) probabilistic first-order logic with temporal operators, interpreted over fixed-length initial segments of (discrete) time. Given a formula φ of the resulting logic and a natural number N, we ask: is φ satisfiable over a space of length N + 1 sequences of states (first-order structures)? We show the problem to be decidable for monodic fragments of the logic whose first-order part has a decidable satisfiability problem and we also establish the problem's computational complexity when the first-order part is among some well-known decidable fragments of first-order logic.

We introduce a variant of a formalism appearing in recent work geared towards modelling systems in which a distinguished entity (leader) orchestrates the operation of an arbitrary number of identical entities (followers). Our variant is better suited for the verification of system properties involving complex arithmetic conditions. Whereas the original formalism is translated into a tractable fragment of first-order temporal logic, aiming to utilize automated (first-order temporal logic) theorem provers for verification, our variant is translated into linear integer arithmetic, aiming to utilize satisfiability modulo theories (SMT) solvers for verification. In particular, for any given system specified in our formalism, we prove, for any natural numbern, the existence of a linear integer arithmetic formula whose models are in one-to-one correspondence with certain counting abstractions (profiles) of executions of the system forntime steps. Thus, one is able to verify, for any natural numbern, that all executions forntime steps of any such system have a given property by establishing that said formula logically entails the property. To highlight the practical utility of our approach, we specify and verify three consensus protocols, actively used in distributed database systems and low-power wireless networks.

Abstract We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol’s translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.

This paper develops a formal framework, founded on description logics, to assist decision making in relation to the manufacturing operation and control in modern enterprises that stand to benefit from the transition to Industry 4.0. The objective is to provide sophisticated support to individuals making decisions in the area of production operations management and in particular, production scheduling and material requirements planning. Using this framework, this paper demonstrates an approach to encode the domain knowledge of human experts managing the production as sets of formal rules. These rules can be implemented in an intelligent system that can assist and empower human experts, reducing difficulty when making decisions in complex manufacturing environments.

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.