LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
Abstract—We investigate some basic questions about the interaction of regular and rational relations on words. The primary motivation comes from the study of logics for querying ...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has ofte...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
Abstract—A bicategory of concurrent games, where nondeterministic strategies are formalized as certain maps of event structures, was introduced recently. This paper studies an ex...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—We show that if a finite relational structure has a near unanimity polymorphism, then the constraint satisfaction problem with that structure as its fixed template has bounded...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the s...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This al...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—We show how to reliably compute fast-growing functions with timed-arc Petri nets and data nets. This construction provides ordinal-recursive lower bounds on the complexity of th...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value infinite domain. They have been used as an abstraction mode...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—A novel countermodel-producing decision procedure that applies to several multi-modal logics, both intuitionistic and classical, is presented. Based on backwards search in label...
LICS
2012
IEEE
11 years 7 months ago
2012
IEEE
—We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types...