Proceedings - Symposium on Logic in Computer Science
SCOPUS (1986-1987,1990-2011,2013,2015-2019,2021-2024)
1043-6871
Mỹ
Cơ quản chủ quản: Institute of Electrical and Electronics Engineers Inc.
Lĩnh vực:
SoftwareMathematics (miscellaneous)
Phân tích ảnh hưởng
Các bài báo tiêu biểu
Remarks on isomorphisms in typed lambda calculi with empty and sum types
- Trang 147-156
Tarski asked whether the arithmetic identities taught in high school are
complete for showing all arithmetic equations valid for the natural numbers. The
answer to this question for the language of arithmetic expressions using a
constant for the number one and the operations of product and exponentiation is
affirmative, and the complete equational theory also characterises isomorphism
in the typed...
#Equations #Digital arithmetic #Educational institutions #Computer languages #Calculus #Logic programming #Functional programming #Algebra #Laboratories #Libraries
Tree extension algebras: logics, automata, and query languages
- Trang 203-212
We study relations on trees defined by first-order constraints over a vocabulary
that includes the tree extension relation T...
#Algebra #Logic functions #Automata #Database languages #XML #Query processing #Logic programming #Computer science #Transducers #Vocabulary
The metric analogue of weak bisimulation for probabilistic processes
- Trang 413-422
We observe that equivalence is not a robust concept in the presence of numerical
information - such as probabilities-in the model. We develop a metric analogue
of weak bisimulation in the spirit of our earlier work on metric analogues for
strong bisimulation. We give a fixed point characterization of the metric. This
makes available conductive reasoning principles and allows us to prove metric
ana...
#Computer science #Probability distribution #Robustness #Channel capacity #Concurrent computing #Distributed computing #Stochastic systems #State-space methods #Logic #Boolean functions
Decidable and undecidable fragments of first-order branching temporal logics
- Trang 393-402
In this paper we analyze the decision problem for fragments of first-order
extensions of branching time temporal logics such as computational tree logics
CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one
hand, we show that the one-variable fragments of logics like first-order
CTL*-such as the product of propositional CTL* with simple propositional modal
logic S5, or even ...
#Logic #Computer science #Educational institutions #Knowledge representation #Application software #Turning #History
Temporal logic with forgettable past
- Trang 383-392
We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL
can be exponentially more succinct than LTL+Past (which in turn can be more
succinct than LTL). We study satisfiability and model checking for NLTL and
provide optimal automata-theoretic algorithms for these EXPSPACE-complete
problems.
#Automatic logic units #Computer science #Polynomials
Complete problems for dynamic complexity classes
- Trang 313-322
We present the first complete problems for dynamic complexity classes including
the classes Dyn-FO and Dyn-ThC/sup 0/, the dynamic classes corresponding to
relational calculus and (polynomially bounded) SQL, respectively. The first
problem we show complete for Dyn-FO is a single-step version of the circuit
value problem (SSCV). Of independent interest, our construction also produces a
first-order ...
#Polynomials #Computer science #Complexity theory #Databases #Heuristic algorithms #Data structures #Logic #Calculus #Circuits #Application software
Dense real-time games
- Trang 167-176
The rapid development of complex and safety-critical systems requires the use of
reliable verification methods and tools for system design (synthesis). Many
systems of interest are reactive, in the sense that their behavior depends on
the interaction with the environment. A natural framework to model them is a
two-player game: the system versus the environment. In this context, the central
problem...
#Automata #Clocks #Logic #Timing #Computer science #Open systems #Real time systems #Tree graphs #Indium tin oxide #Game theory
A fully abstract may testing semantics for concurrent objects
- Trang 101-112
This paper provides a fully abstract semantics for a variant of the concurrent
object calculus. We define may testing for concurrent object components and then
characterise it using a trace semantics inspired by UML interaction diagrams.
The main result of this paper is to show that the trace semantics is fully
abstract for may testing. This is the first such result for a concurrent object
languag...
#Testing #Calculus #Unified modeling language #Yarn #Production facilities #Safety #Robustness #Visualization #Jacobian matrices #Standards development
The complexity of first-order and monadic second-order logic revisited
- Trang 215-224
The model-checking problem for a logic L on a class C of structures asks whether
a given L-sentence holds in a given structure in C. In this paper, we give
super-exponential lower bounds for fixed-parameter tractable model-checking
problems for first-order and monadic second-order logic. We show that unless
PTIME=NP, the model-checking problem for monadic second-order logic on finite
words is not ...
#Logic #Complexity theory #Polynomials #Databases #Computer science #Informatics #Upper bound #Artificial intelligence #State-space methods
Domain theory and differential calculus (functions of one variable)
- Trang 277-286
A data-type for differential calculus is introduced, which is based on domain
theory. We define the integral and also the derivative of a Scott continuous
function on the domain of intervals, and present a domain-theoretic
generalization of the fundamental theorem of calculus. We then construct a
domain for differentiable real valued functions of a real variable. The set of
classical C/sup 1/ func...
#Calculus #Differential equations #Polynomials #Educational institutions #Pathology #Mathematics #Approximation algorithms #Uncertainty #Application software #Logic design