Proceedings - Symposium on Logic in Computer Science
SCOPUS (1986-1987,1990-2011,2013,2015-2019,2021-2023)
1043-6871
Mỹ
Cơ quản chủ quản: Institute of Electrical and Electronics Engineers Inc.
Lĩnh vực:
SoftwareMathematics (miscellaneous)
Các bài báo tiêu biểu
Tree-like counterexamples in model checking
- Trang 19-29
Counter examples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework ...... hiện toàn bộ
#Logic #Computer science #Switches #Art #Intelligent networks #Computer networks #Debugging #Contracts #Government
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 ...... hiện toàn bộ
#Logic #Complexity theory #Polynomials #Databases #Computer science #Informatics #Upper bound #Artificial intelligence #State-space methods
Semantics and logic of object calculi
- Trang 113-122
The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic for the object calculus and to suggest possible extensions. For the purposes of this discussio...... hiện toàn bộ
#Logic programming #Calculus #Object oriented programming #Machinery #Object oriented modeling #Computer science
Logic phân tách: một logic cho cấu trúc dữ liệu có thể biến đổi chia sẻ Dịch bởi AI
- Trang 55-74
Trong công trình hợp tác với Peter O'Hearn và những người khác, dựa trên những ý tưởng ban đầu của Burstall, chúng tôi đã phát triển một mở rộng của logic Hoare cho phép lập luận về các chương trình lệnh cấp thấp sử dụng cấu trúc dữ liệu có thể thay đổi được chia sẻ. Ngôn ngữ lập trình lệnh đơn giản được mở rộng với các lệnh (không phải biểu thức) để truy cập và sửa đổi các cấu trúc chia sẻ, cũng ...... hiện toàn bộ
#Data structures #Computer science #Programmable logic arrays #Reflection #Logic programming #Computer languages #Logic arrays #Arithmetic #Artificial intelligence #Bibliographies
Modal and guarded characterisation theorems over finite transition systems
- Trang 371-380
Characterisation theorems for modal and guarded fragments of first-order logic are explored over finite transition systems. We show that the classical characterisations in terms of semantic invariance under the appropriate forms of bisimulation equivalence can be recovered at the level of finite model theory. The new, more constructive proofs naturally extend to alternative proofs of the classical...... hiện toàn bộ
#Logic #H infinity control #Game theory #Computer science
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 ...... hiện toàn bộ
#Polynomials #Computer science #Complexity theory #Databases #Heuristic algorithms #Data structures #Logic #Calculus #Circuits #Application software
Observational equivalence of 3rd-order Idealized Algol is decidable
- Trang 245-256
We prove that observational equivalence of 3rd-order finitary Idealized Algol (IA) is decidable using Game Semantics. By modelling state explicitly in our games, we show that the denotation of a term M of this fragment of IA (built up from finite base types) is a compactly innocent strategy-with-state i.e. the strategy is generated by a finite view function f/sub M/. Given any such f/sub M/, we co...... hiện toàn bộ
#Computer languages #Laboratories #Automata #Character recognition #Concrete #Application software #Computer applications #Algorithm design and analysis #Hardware #Data security
Some results on automatic structures
- Trang 235-242
We study the class of countable structures which can be presented by synchronous finite automata. We reduce the problem of existence of an automatic presentation of a structure to that for a graph. We exhibit a series of properties of automatic equivalence structures, linearly ordered sets and permutation structures. These serve as a first step in producing practical descriptions of some automatic...... hiện toàn bộ
#Automata #Computer science #Mathematics #Terminology #Automatic logic units #Polynomials
Separability, expressiveness, and decidability in the ambient logic
- Trang 423-432
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (=/sub L/). We consider MA, and two Turing complete subsets of...... hiện toàn bộ
#Logic #Chromium #Calculus #Database languages #Switches #Computer science #Query processing #Shape
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...... hiện toàn bộ
#Testing #Calculus #Unified modeling language #Yarn #Production facilities #Safety #Robustness #Visualization #Jacobian matrices #Standards development